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₁[ 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₁[mm,x,y]

proof

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₁[mm,x,y]
let x be Element of Funcs ((AllTermsOf S),U); :: thesis: ex y being Element of Funcs ((AllTermsOf S),U) st S₁[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₁[mm,x,yyy]
thus S₁[mm,x,yyy] ; :: thesis: verum

end;

consider f being sequence of (Funcs ((AllTermsOf S),U)) such that
A2: ( f . 0 = fzzz & ( for mm being Nat holds S₁[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