let i be Nat; for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() 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 ; for o being OperSymbol of S
for X being V5() 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; for X being V5() 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 V5() 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 p be Element of Args (o,(Free (S,X))); ( 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 ) )
; 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 }
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 H1( 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
H1(i) misses H1(j)
A7:
for i being Nat st i < len f holds
card H1(i) = f . (i + 1)
card (union { H1(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; verum