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 S1[ 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 S1[mm,x,y]
proof
let mm be
Nat;
for x being Element of Funcs ((AllTermsOf S),U) ex y being Element of Funcs ((AllTermsOf S),U) st S1[mm,x,y]let x be
Element of
Funcs (
(AllTermsOf S),
U);
ex y being Element of Funcs ((AllTermsOf S),U) st S1[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
;
S1[mm,x,yyy]
thus
S1[
mm,
x,
yyy]
;
verum
end;
consider f being sequence of (Funcs ((AllTermsOf S),U)) such that
A2:
( f . 0 = fzzz & ( for mm being Nat holds S1[mm,f . mm,f . (mm + 1)] ) )
from RECDEF_1:sch 2(A1);
take
f
; ( 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; verum