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 = () --> u;
defpred S1[ set , Element of Funcs ((),U), set ] means \$3 = ^^^(I * ()),^^^\$2,()____;
reconsider fzz = () --> u as Function of (),U ;
reconsider fzzz = fzz as Element of Funcs ((),U) by FUNCT_2:8;
A1: for mm being Nat
for x being Element of Funcs ((),U) ex y being Element of Funcs ((),U) st S1[mm,x,y]
proof
let mm be Nat; :: thesis: for x being Element of Funcs ((),U) ex y being Element of Funcs ((),U) st S1[mm,x,y]
let x be Element of Funcs ((),U); :: thesis: ex y being Element of Funcs ((),U) st S1[mm,x,y]
reconsider xx = x as Function of (),U ;
reconsider yy = ^^^(I * ()),^^^xx,()____ as Function of (),U by Lm4;
reconsider yyy = yy as Element of Funcs ((),U) by FUNCT_2:8;
take yyy ; :: thesis: S1[mm,x,yyy]
thus S1[mm,x,yyy] ; :: thesis: verum
end;
consider f being sequence of (Funcs ((),U)) such that
A2: ( f . 0 = fzzz & ( for mm being Nat holds S1[mm,f . mm,f . (mm + 1)] ) ) from take f ; :: thesis: ( f . 0 = () --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * ()),^^^(f . mm),()____ ) )
thus ( f . 0 = () --> u & ( for mm being Element of NAT holds f . (mm + 1) = ^^^(I * ()),^^^(f . mm),()____ ) ) by A2; :: thesis: verum