Введение в универсальную и категорную алгебру. Тронин С.Н. - 26 стр.

u = w10 : : : wm00 ;1 = w100 : : : wm00 ;1 , I K \TOMU SLOWU DLINY `(w) ; 1 PRI-
MENIMO PREDPOLOVENIE INDUKCII. dOPUSTIM, ^TO HOTQ BY ODNO IZ
SLOW u0 , u00 NEPUSTO, NAPRIMER, NEPUSTO u0 . sNA^ALA RAZBEREM SLU^AJ
val(c) = 1 . tAK KAK wm0 I wm00 ESTX  -SLOWA, TO WALENTNOSTX IH LE-
WYH OTREZKOW u0 I u00 DOLVNA BYTX STROGO POLOVITELXNOJ, NO TOGDA
RAWENSTWO 1 = val(wm0 ) = val(u0 ) + val(c) PRIWODIT K PROTIWORE^I@.
rASSMOTRIM SLU^AJ val(c) = 1 ; n , n  1 . iZ RAWENSTW
 val(w) = m = val(w10 : : :wm0 ;1 )+ val(u0 )+ val(c) = m ; 1+ val(u0 )+1 ; n
DELAEM WYWOD, ^TO val(u0) = n  1 , I ANALOGI^NO val(u00 ) = n . eSLI
(u0 )(j) | LEWYJ OTREZOK u0 , TO \TO TAKVE LEWYJ OTREZOK  -SLOWA wm0 ,
PO\TOMU val((u0 )(j) ) > 0 . |TO ZNA^IT, ^TO u0 = u01 : : : u0n , GDE KAVDOE
u0i ESTX  -SLOWO. aNALOGI^NYM OBRAZOM POLU^AEM, ^TO u00 = u100 : : : u00n ,
GDE KAVDOE u00i ESTX  -SLOWO. pO\TOMU RAWENSTWO u = w10 : : : wm00 ;1u0 =
w100 : : : wm00 ;1u00 PEREPIETSQ WIDE
     u = w10 : : : wm00 ;1u01 : : : u0n = w100 : : : wm00 ;1u001 : : : u00n .
k \TOMU SLOWU PRIMENIMO PREDPOLOVENIE INDUKCII, TAK ^TO w10 =
w100 , : : : , wm0 ;1 = wm00 ;1 , u01 = u001 , : : : , u0n = u00n . oTS@DA u0 = u00 ,
wm0 = u0 c = u00 c = wm00 .
    2) eSLI w = w10 : : : wm0 !0 = w100 : : : wk00!00 , TO !0 = !00 | ODIN I TOT
VE SIMWOL IZ  . oTS@DA w10 : : :wm0 = w100 : : :wk00 , I MOVNO PRIMENITX
PERWOE UTWERVDENIE LEMMY.
    tEPERX MOVNO WERNUTXSQ K MNOGOSORTNOMU SLU^A@ (PROIZWOLXNOE
MNOVESTWO S ). pUSTX X = fXsjs 2 S g , F = fFs js 2 S g | ALGEBRA
MNOGOSORTNYH  -SLOW. pOLOVIM X = s2S Xs , n = s :::snj2S s :::snj ,
                                                                1
                                                                             1

n  0 . pUSTX 0 = n0 n . tOGDA MOVNO POSTROITX ALGEBRU F 0 ODNO-
SORTNYH 0 -SLOW S BAZISOM X . iZ POSTROENIQ WIDNO, ^TO s2S Fs  F 0 ,
HOTQ \TO WKL@^ENIE, WOOB]E GOWORQ, NE OBQZANO BYTX RAWENSTWOM.
iNYMI SLOWAMI, KAVDOE MNOGOSORTNOE  -SLOWO BUDET 0 -SLOWOM, I
PO\TOMU K NEMU PRIMENIMY REZULXTATY PUNKTOW 1) I 2) DLQ ODNO-
SORTNOGO SLU^AQ. lEMMA DOKAZANA.
  pUSTX X | GRADUIROWANNOE MNOVESTWO, F = Fr (X) = Fr(X) |
ALGEBRA MNOGOSORTNYH  -SLOW. pO POSTROENI@, DLQ KAVDOGO s 2 S
IMEETSQ WKL@^ENIE s = s (X) : Xs  Fs = (F)s . ~EREZ  = (X) BU-
DEM OBOZNA^ATX SOOTWETSTWU@]EE OTOBRAVENIE GRADUIROWANNYH MNO-
VESTW X ;! Fr(X) . dOKAVEM, ^TO WYPOLNENO SLEDU@]EE UNIWER-
                                         26