let i be Nat; :: thesis: for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1
let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) implies deg (o -term p) = i + 1 )
given f being FinSequence of NAT such that A1: ( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) ; :: thesis: deg (o -term p) = i + 1
dom f = dom p by A1, MSUALG_3:6;
then A2: len f = len p by FINSEQ_3:29;
set t = o -term p;
set I = [: the carrier' of S,{ the carrier of S}:];
set A = { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } ;
A4: {} nin union { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p }

proof

assume {} in union { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } ; :: thesis: contradiction
then consider J being set such that
A1: ( {} in J & J in { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } ) by TARSKI:def 4;
consider i being Nat such that
A2: ( J = <*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:]) & i < len p ) by A1;
consider q being Element of (p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:] such that
A3: ( {} = <*i*> ^ q & q in (p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:] ) by A1, A2;
thus contradiction by A3; :: thesis: verum

end;

reconsider J = [o, the carrier of S] as set ;
J in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:106;
then IFIN (J,[: the carrier' of S,{ the carrier of S}:],{{}},{}) = {{}} by MATRIX_7:def 1;
then (o -term p) " [: the carrier' of S,{ the carrier of S}:] = {{}} \/ (union { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } ) by Th80;
then A5: card ((o -term p) " [: the carrier' of S,{ the carrier of S}:]) = (card {{}}) +` (card (union { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } )) by A4, CARD_2:35, ZFMISC_1:50
.= 1 +` (card (union { (<*i*> ^^ ((p . (i + 1)) " [: the carrier' of S,{ the carrier of S}:])) where i is Nat : i < len p } )) by CARD_1:30 ;
deffunc H₁( Nat) -> set = <*$1*> ^^ ((p . ($1 + 1)) " [: the carrier' of S,{ the carrier of S}:]);
A6: for i, j being Nat st i < len f & j < len f & i <> j holds
H₁(i) misses H₁(j)

proof

let i, j be Nat; :: thesis: ( i < len f & j < len f & i <> j implies H₁(i) misses H₁(j) )
B1: ( len <*i*> = 1 & 1 = len <*j*> & <*i*> . 1 = i & <*j*> . 1 = j ) by FINSEQ_1:40;
thus ( i < len f & j < len f & i <> j implies H₁(i) misses H₁(j) ) by B1, Th2; :: thesis: verum

end;

A7: for i being Nat st i < len f holds
card H₁(i) = f . (i + 1)

proof

let i be Nat; :: thesis: ( i < len f implies card H₁(i) = f . (i + 1) )
assume i < len f ; :: thesis: card H₁(i) = f . (i + 1)
then A9: ( 1 <= i + 1 & i + 1 <= len f ) by NAT_1:12, NAT_1:13;
reconsider t = p . (i + 1) as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. (i + 1)) by A1, A9, FINSEQ_3:25, MSUALG_6:2;
f . (i + 1) = deg t by A1, A9, FINSEQ_3:25;
hence card H₁(i) = f . (i + 1) by Th1; :: thesis: verum

end;

card (union { H₁(i) where i is Nat : i < len f } ) = Sum f from MSAFREE5:sch 1(A6, A7);
then card ((o -term p) " [: the carrier' of S,{ the carrier of S}:]) = 1 +` (Sum f) by A2, A5;
hence deg (o -term p) = i + 1 by A1; :: thesis: verum