set A = AllTermsOf S;

set F = S -firstChar ;

set ST = S -subTerms ;

set SS = AllSymbolsOf S;

set Z = AtomicTermsOf S;

set T = S -termsOfMaxDepth ;

set fz = (AllTermsOf S) --> u;

defpred S_{1}[ set , Element of Funcs ((AllTermsOf S),U), set ] means $3 = ^^^(I * (S -firstChar)),^^^$2,(S -subTerms)____;

reconsider fzz = (AllTermsOf S) --> u as Function of (AllTermsOf S),U ;

reconsider fzzz = fzz as Element of Funcs ((AllTermsOf S),U) by FUNCT_2:8;

A1: for mm being Nat

for x being Element of Funcs ((AllTermsOf S),U) ex y being Element of Funcs ((AllTermsOf S),U) st S_{1}[mm,x,y]

A2: ( f . 0 = fzzz & ( for mm being Nat holds S_{1}[mm,f . mm,f . (mm + 1)] ) )
from RECDEF_1:sch 2(A1);

take f ; :: thesis: ( f . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * (S -firstChar)),^^^(f . mm),(S -subTerms)____ ) )

thus ( f . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * (S -firstChar)),^^^(f . mm),(S -subTerms)____ ) ) by A2; :: thesis: verum

set F = S -firstChar ;

set ST = S -subTerms ;

set SS = AllSymbolsOf S;

set Z = AtomicTermsOf S;

set T = S -termsOfMaxDepth ;

set fz = (AllTermsOf S) --> u;

defpred S

reconsider fzz = (AllTermsOf S) --> u as Function of (AllTermsOf S),U ;

reconsider fzzz = fzz as Element of Funcs ((AllTermsOf S),U) by FUNCT_2:8;

A1: for mm being Nat

for x being Element of Funcs ((AllTermsOf S),U) ex y being Element of Funcs ((AllTermsOf S),U) st S

proof

consider f being sequence of (Funcs ((AllTermsOf S),U)) such that
let mm be Nat; :: thesis: for x being Element of Funcs ((AllTermsOf S),U) ex y being Element of Funcs ((AllTermsOf S),U) st S_{1}[mm,x,y]

let x be Element of Funcs ((AllTermsOf S),U); :: thesis: ex y being Element of Funcs ((AllTermsOf S),U) st S_{1}[mm,x,y]

reconsider xx = x as Function of (AllTermsOf S),U ;

reconsider yy = ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ as Function of (AllTermsOf S),U by Lm4;

reconsider yyy = yy as Element of Funcs ((AllTermsOf S),U) by FUNCT_2:8;

take yyy ; :: thesis: S_{1}[mm,x,yyy]

thus S_{1}[mm,x,yyy]
; :: thesis: verum

end;let x be Element of Funcs ((AllTermsOf S),U); :: thesis: ex y being Element of Funcs ((AllTermsOf S),U) st S

reconsider xx = x as Function of (AllTermsOf S),U ;

reconsider yy = ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ as Function of (AllTermsOf S),U by Lm4;

reconsider yyy = yy as Element of Funcs ((AllTermsOf S),U) by FUNCT_2:8;

take yyy ; :: thesis: S

thus S

A2: ( f . 0 = fzzz & ( for mm being Nat holds S

take f ; :: thesis: ( f . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * (S -firstChar)),^^^(f . mm),(S -subTerms)____ ) )

thus ( f . 0 = (AllTermsOf S) --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * (S -firstChar)),^^^(f . mm),(S -subTerms)____ ) ) by A2; :: thesis: verum