let U be non empty set ; :: thesis:
let S1, S2 be Language; :: thesis:
set II1 = U -InterpretersOf S1;
set II2 = U -InterpretersOf S2;
set N1 = TheNorSymbOf S1;
set N2 = TheNorSymbOf S2;
set F1 = S1 -firstChar ;
set F2 = S2 -firstChar ;
set a1 = the adicity of S1;
set a2 = the adicity of S2;
set O1 = OwnSymbolsOf S1;
set O2 = OwnSymbolsOf S2;
set d = U -deltaInterpreter ;
set E1 = TheEqSymbOf S1;
set E2 = TheEqSymbOf S2;
set AS1 = AtomicFormulaSymbolsOf S1;
set AS2 = AtomicFormulaSymbolsOf S2;
assume A1: TheNorSymbOf S1 = TheNorSymbOf S2 ; :: thesis:
assume A2: ( TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) ) ; :: thesis:
defpred S₁[ Nat] means for I1 being Element of U -InterpretersOf S1
for I2 being Element of U -InterpretersOf S2
for phi1 being $1 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds
ex phi2 being $1 -wff string of S2 st
( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 );
A3: S₁[ 0 ]

let I1 be Element of U -InterpretersOf S1; :: thesis:
let I2 be Element of U -InterpretersOf S2; :: thesis:
let phi1 be 0 -wff string of S1; :: thesis:
set TE1 = I1 -TermEval ;
set TE2 = I2 -TermEval ;
set X = rng phi1;
reconsider XX = (rng phi1) /\ (OwnSymbolsOf S1) as Subset of (OwnSymbolsOf S1) ;
reconsider r1 = (S1 -firstChar) . phi1 as relational Element of S1 ;
A4: the adicity of S1 | XX = ( the adicity of S1 | (OwnSymbolsOf S1)) | (rng phi1) by RELAT_1:71
.= the adicity of S2 | XX by A2, RELAT_1:71 ;
assume I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ; :: thesis:
then (I2 | (OwnSymbolsOf S1)) | (rng phi1) = I1 | XX by RELAT_1:71;
then I1 | XX = I2 | XX by RELAT_1:71;
then consider phi2 being 0wff string of S2 such that
A5: ( phi2 = phi1 & I2 -AtomicEval phi2 = I1 -AtomicEval phi1 ) by A4, Lm48, A2;
reconsider phi2 = phi2 as 0 -wff string of S2 ;
take phi2 ; :: thesis:
set st1 = SubTerms phi1;
set st2 = SubTerms phi2;
reconsider r2 = (S2 -firstChar) . phi2 as relational Element of S2 ;
thus ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) by A5; :: thesis:

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:
let I1 be Element of U -InterpretersOf S1; :: thesis:
let I2 be Element of U -InterpretersOf S2; :: thesis:
let phi1 be n + 1 -wff string of S1; :: thesis:
set X = rng phi1;
assume A8: I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ; :: thesis:
reconsider h1 = head phi1 as n -wff string of S1 ;
set t = tail phi1;
set s1 = (S1 -firstChar) . phi1;
consider h2 being n -wff string of S2 such that
A9: ( h1 = h2 & I1 -TruthEval h1 = I2 -TruthEval h2 ) by A7, A8;

then reconsider phi11 = phi1 as n + 1 -wff exal string of S1 ;
reconsider l1 = (S1 -firstChar) . phi11 as literal Element of S1 ;
A10: I1 . l1 = I2 . l1 by A8, FOMODEL1:def 19, FUNCT_1:49;
l1 in dom I2 by A10, FUNCT_1:def 2;
then l1 in OwnSymbolsOf S2 ;
then reconsider l2 = l1 as own Element of S2 ;
|.(ar l2).| -tuples_on U = dom (I2 . l2) by PARTFUN1:def 2
.= 0 -tuples_on U by A10, FUNCT_2:def 1 ;
then ( not l2 is relational & not l2 is operational ) ;
then reconsider l2 = l2 as literal Element of S2 ;
reconsider phi2 = <*l2*> ^ h2 as n + 1 -wff exal string of S2 ;
take phi2 ; :: thesis:
A11: phi1 = (<*l1*> ^ h1) ^ (tail phi11) by FOMODEL2:23
.= <*l1*> ^ h1 ;
hence phi1 = phi2 by A9; :: thesis:
( I1 -TruthEval phi11 = 1 iff I2 -TruthEval phi2 = 1 )

assume I1 -TruthEval phi11 = 1 ; :: thesis:
then consider u being Element of U such that
A12: ((l1,u) ReassignIn I1) -TruthEval h1 = 1 by FOMODEL2:19, A11;
reconsider I11 = (l1,u) ReassignIn I1 as Element of U -InterpretersOf S1 ;
reconsider I22 = (l2,u) ReassignIn I2 as Element of U -InterpretersOf S2 ;
I11 | (OwnSymbolsOf S1) = (I1 | (OwnSymbolsOf S1)) +* ((l1 .--> ({} .--> u)) | (OwnSymbolsOf S1)) by FUNCT_4:71
.= I22 | (OwnSymbolsOf S1) by A8, FUNCT_4:71 ;
then consider h22 being n -wff string of S2 such that
A13: ( h22 = h1 & I11 -TruthEval h1 = I22 -TruthEval h22 ) by A7;
thus I2 -TruthEval phi2 = 1 by FOMODEL2:19, A13, A9, A12; :: thesis:

end;

assume I2 -TruthEval phi2 = 1 ; :: thesis:
then consider u2 being Element of U such that
A14: ((l2,u2) ReassignIn I2) -TruthEval h2 = 1 by FOMODEL2:19;
reconsider I11 = (l1,u2) ReassignIn I1 as Element of U -InterpretersOf S1 ;
reconsider I22 = (l2,u2) ReassignIn I2 as Element of U -InterpretersOf S2 ;
I11 | (OwnSymbolsOf S1) = (I1 | (OwnSymbolsOf S1)) +* ((l1 .--> ({} .--> u2)) | (OwnSymbolsOf S1)) by FUNCT_4:71
.= I22 | (OwnSymbolsOf S1) by A8, FUNCT_4:71 ;
then consider h222 being n -wff string of S2 such that
A15: ( h222 = h1 & I11 -TruthEval h1 = I22 -TruthEval h222 ) by A7;
thus I1 -TruthEval phi11 = 1 by FOMODEL2:19, A11, A14, A15, A9; :: thesis:

end;

end;

then reconsider phi11 = phi1 as non 0wff n + 1 -wff non exal string of S1 ;
reconsider t1 = tail phi11 as n -wff string of S1 ;
consider t2 being n -wff string of S2 such that
A16: ( t1 = t2 & I1 -TruthEval t1 = I2 -TruthEval t2 ) by A7, A8;
reconsider phi2 = (<*(TheNorSymbOf S2)*> ^ h2) ^ t2 as non 0wff n + 1 -wff non exal string of S2 ;
take phi2 ; :: thesis:
( ((S1 -firstChar) . phi11) \+\ (TheNorSymbOf S1) = {} & ((S2 -firstChar) . phi2) \+\ (TheNorSymbOf S2) = {} ) ;
then A17: ( (S1 -firstChar) . phi1 = TheNorSymbOf S1 & (S2 -firstChar) . phi2 = TheNorSymbOf S2 & phi11 = (<*((S1 -firstChar) . phi11)*> ^ h1) ^ t1 & h2 = head phi2 & t2 = tail phi2 ) by FOMODEL2:23, FOMODEL0:29;
hence phi1 = phi2 by A16, A9, A1; :: thesis:
set b1 = I1 -TruthEval h1;
set c1 = I1 -TruthEval t1;
set b2 = I2 -TruthEval h2;
set c2 = I2 -TruthEval t2;
set A1 = I1 -TruthEval phi11;
set A2 = I2 -TruthEval phi2;
( (I1 -TruthEval phi11) \+\ ((I1 -TruthEval (head phi11)) 'nor' (I1 -TruthEval (tail phi11))) = {} & (I2 -TruthEval phi2) \+\ ((I2 -TruthEval (head phi2)) 'nor' (I2 -TruthEval (tail phi2))) = {} ) ;
then ( I1 -TruthEval phi11 = (I1 -TruthEval h1) 'nor' (I1 -TruthEval t1) & I2 -TruthEval phi2 = (I2 -TruthEval h2) 'nor' (I2 -TruthEval t2) ) by A17, FOMODEL0:29;
hence I1 -TruthEval phi1 = I2 -TruthEval phi2 by A9, A16; :: thesis:

end;

then consider phi2 being 0 -wff string of S2 such that
A18: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) by A3, A8;
phi2 is 0 + (0 * (n + 1)) -wff ;
then phi2 is 0 + (n + 1) -wff ;
then reconsider phi22 = phi2 as n + 1 -wff string of S2 ;
take phi22 ; :: thesis:
thus ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by A18; :: thesis:

end;

A19: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
let I1 be Element of U -InterpretersOf S1; :: thesis:
let I2 be Element of U -InterpretersOf S2; :: thesis:
let phi1 be wff string of S1; :: thesis:
set d = Depth phi1;
reconsider phi11 = phi1 null 0 as (Depth phi1) + 0 -wff string of S1 ;
assume I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ; :: thesis:
then ex phi2 being Depth phi1 -wff string of S2 st
( phi2 = phi11 & I2 -TruthEval phi2 = I1 -TruthEval phi11 ) by A19;
hence ex phi2 being wff string of S2 st
( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) ; :: thesis: