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;
reconsider fzz = () --> u as Element of Funcs ((),U) by FUNCT_2:8;
defpred S1[ set , set , set ] means for f being Element of Funcs ((),U) st \$2 = f holds
\$3 = ^^^(I * ()),^^^f,()____;
let IT1, IT2 be sequence of (Funcs ((),U)); :: thesis: ( IT1 . 0 = () --> u & ( for mm being Element of NAT holds IT1 . (mm + 1) = ^^^(I * ()),^^^(IT1 . mm),()____ ) & IT2 . 0 = () --> u & ( for mm being Element of NAT holds IT2 . (mm + 1) = ^^^(I * ()),^^^(IT2 . mm),()____ ) implies IT1 = IT2 )
assume A3: ( IT1 . 0 = () --> u & ( for mm being Element of NAT holds IT1 . (mm + 1) = ^^^(I * ()),^^^(IT1 . mm),()____ ) ) ; :: thesis: ( not IT2 . 0 = () --> u or ex mm being Element of NAT st not IT2 . (mm + 1) = ^^^(I * ()),^^^(IT2 . mm),()____ or IT1 = IT2 )
assume A4: ( IT2 . 0 = () --> u & ( for mm being Element of NAT holds IT2 . (mm + 1) = ^^^(I * ()),^^^(IT2 . mm),()____ ) ) ; :: thesis: IT1 = IT2
A5: IT1 . 0 = fzz by A3;
A6: for m being Nat holds S1[m,IT1 . m,IT1 . (m + 1)]
proof
let m be Nat; :: thesis: S1[m,IT1 . m,IT1 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of Funcs ((),U); :: thesis: ( IT1 . m = f implies IT1 . (m + 1) = ^^^(I * ()),^^^f,()____ )
assume IT1 . m = f ; :: thesis: IT1 . (m + 1) = ^^^(I * ()),^^^f,()____
then IT1 . mm = f ;
hence IT1 . (m + 1) = ^^^(I * ()),^^^f,()____ by A3; :: thesis: verum
end;
A7: IT2 . 0 = fzz by A4;
A8: for m being Nat holds S1[m,IT2 . m,IT2 . (m + 1)]
proof
let m be Nat; :: thesis: S1[m,IT2 . m,IT2 . (m + 1)]
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
let f be Element of Funcs ((),U); :: thesis: ( IT2 . m = f implies IT2 . (m + 1) = ^^^(I * ()),^^^f,()____ )
assume IT2 . m = f ; :: thesis: IT2 . (m + 1) = ^^^(I * ()),^^^f,()____
then IT2 . mm = f ;
hence IT2 . (m + 1) = ^^^(I * ()),^^^f,()____ by A4; :: thesis: verum
end;
A9: for m being Nat
for x, y1, y2 being Element of Funcs ((),U) st S1[m,x,y1] & S1[m,x,y2] holds
y1 = y2
proof
let m be Nat; :: thesis: for x, y1, y2 being Element of Funcs ((),U) st S1[m,x,y1] & S1[m,x,y2] holds
y1 = y2

let x, y1, y2 be Element of Funcs ((),U); :: thesis: ( S1[m,x,y1] & S1[m,x,y2] implies y1 = y2 )
assume for f being Element of Funcs ((),U) st x = f holds
y1 = ^^^(I * ()),^^^f,()____ ; :: thesis: ( not S1[m,x,y2] or y1 = y2 )
then A10: y1 = ^^^(I * ()),^^^x,()____ ;
assume for f being Element of Funcs ((),U) st x = f holds
y2 = ^^^(I * ()),^^^f,()____ ; :: thesis: y1 = y2
hence y1 = y2 by A10; :: thesis: verum
end;
IT1 = IT2 from NAT_1:sch 14(A5, A6, A7, A8, A9);
hence IT1 = IT2 ; :: thesis: verum