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