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 S₁[ 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 Function of NAT,(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 B1: ( 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 B2: ( 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
C1: IT1 . 0 = fzz by B1;
C2: for m being Nat holds S₁[m,IT1 . m,IT1 . (m + 1)]

proof

let m be Nat; :: thesis: S₁[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 B1; :: thesis: verum

end;

C3: IT2 . 0 = fzz by B2;
C4: for m being Nat holds S₁[m,IT2 . m,IT2 . (m + 1)]

proof

let m be Nat; :: thesis: S₁[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 B2; :: thesis: verum

end;

C5: for m being Nat
for x, y1, y2 being Element of Funcs ((AllTermsOf S),U) st S₁[m,x,y1] & S₁[m,x,y2] holds
y1 = y2

proof

let m be Nat; :: thesis: for x, y1, y2 being Element of Funcs ((AllTermsOf S),U) st S₁[m,x,y1] & S₁[m,x,y2] holds
y1 = y2
let x, y1, y2 be Element of Funcs ((AllTermsOf S),U); :: thesis: ( S₁[m,x,y1] & S₁[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 S₁[m,x,y2] or y1 = y2 )
then D1: 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 D1; :: thesis: verum

end;

IT1 = IT2 from NAT_1:sch 14(C1, C2, C3, C4, C5);
hence IT1 = IT2 ; :: thesis: verum