let U be non empty set ; :: thesis:
let S1, S2 be Language; :: thesis:
set O1 = OwnSymbolsOf S1;
set O2 = OwnSymbolsOf S2;
set a1 = the adicity of S1;
set a2 = the adicity of S2;
set E1 = TheEqSymbOf S1;
set E2 = TheEqSymbOf S2;
set F1 = S1 -firstChar ;
set F2 = S2 -firstChar ;
set AS1 = AtomicFormulaSymbolsOf S1;
set AS2 = AtomicFormulaSymbolsOf S2;
set N1 = TheNorSymbOf S1;
set N2 = TheNorSymbOf S2;
set II1 = U -InterpretersOf S1;
set II2 = U -InterpretersOf S2;
assume A1: ( TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 ) ; :: 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 the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) holds
ex phi2 being $1 -wff string of S2 st phi1 = phi2;
A2: S₁[ 0 ]

proof

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:
reconsider phi11 = phi1 as 0wff string of S1 ;
set x1 = rng phi1;
set x11 = (rng phi1) /\ (OwnSymbolsOf S1);
assume ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) ) ; :: thesis:
then consider phi2 being 0wff string of S2 such that
A3: ( phi11 = phi2 & I1 -AtomicEval phi11 = I2 -AtomicEval phi2 ) by Lm48, A1;
thus ex phi2 being 0 -wff string of S2 st phi1 = phi2 by A3; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
set N = n + 1;
assume A5: 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 x1 = rng phi1;
set x11 = (rng phi1) /\ (OwnSymbolsOf S1);
assume A6: ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) ) ; :: thesis:

per cases ;

suppose phi1 is 0wff ; :: thesis:

then reconsider phi11 = phi1 as 0 -wff string of S1 ;
consider phi2 being 0 -wff string of S2 such that
A7: phi11 = phi2 by A2, A6;
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 by A7; :: thesis:

end;

suppose not phi1 is 0wff ; :: thesis:

then reconsider phi11 = phi1 as non 0wff n + 1 -wff string of S1 ;
reconsider h1 = head phi11 as n -wff string of S1 ;
set t11 = tail phi11;
set l11 = (S1 -firstChar) . phi11;
A8: phi11 = (<*((S1 -firstChar) . phi11)*> ^ h1) ^ (tail phi11) by FOMODEL2:23;
then ( rng h1 c= rng (<*((S1 -firstChar) . phi11)*> ^ h1) & rng (<*((S1 -firstChar) . phi11)*> ^ h1) c= rng phi1 ) by FINSEQ_1:30, FINSEQ_1:29;
then reconsider y1 = rng h1 as non empty Subset of (rng phi1) by XBOOLE_1:1;
reconsider y11 = y1 /\ (OwnSymbolsOf S1) as Subset of ((rng phi1) /\ (OwnSymbolsOf S1)) by XBOOLE_1:26;
A9: I1 | (y11 null ((rng phi1) /\ (OwnSymbolsOf S1))) = (I1 | ((rng phi1) /\ (OwnSymbolsOf S1))) | y11 by RELAT_1:71
.= I2 | (y11 null ((rng phi1) /\ (OwnSymbolsOf S1))) by RELAT_1:71, A6 ;
the adicity of S1 | (y11 null ((rng phi1) /\ (OwnSymbolsOf S1))) = ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1))) | y11 by RELAT_1:71
.= the adicity of S2 | (y11 null ((rng phi1) /\ (OwnSymbolsOf S1))) by RELAT_1:71, A6 ;
then consider h2 being n -wff string of S2 such that
A10: h1 = h2 by A5, A9;

per cases ;

suppose phi11 is exal ; :: thesis:

then reconsider phi11 = phi11 as non 0wff n + 1 -wff exal string of S1 ;
reconsider l1 = (S1 -firstChar) . phi11 as literal Element of S1 ;
phi1 null {} is (rng phi1) \/ {} -valued ;
then {(phi1 . 1)} \ (rng phi1) = {} ;
then phi1 . 1 in rng phi1 by ZFMISC_1:60;
then ( l1 in rng phi1 & l1 in OwnSymbolsOf S1 & dom the adicity of S1 = AtomicFormulaSymbolsOf S1 ) by FOMODEL0:6, FOMODEL1:def 19, FUNCT_2:def 1;
then A11: ( l1 in (rng phi1) /\ (OwnSymbolsOf S1) & dom ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1))) = (AtomicFormulaSymbolsOf S1) /\ ((rng phi1) /\ (OwnSymbolsOf S1)) & l1 in AtomicFormulaSymbolsOf S1 ) by RELAT_1:61, XBOOLE_0:def 4, FOMODEL1:def 20;
then ( l1 in dom ( the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1))) & dom ( the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1))) = ((rng phi1) /\ (OwnSymbolsOf S1)) /\ (dom the adicity of S2) ) by XBOOLE_0:def 4, RELAT_1:61, A6;
then ( l1 in dom the adicity of S2 & dom the adicity of S2 = AtomicFormulaSymbolsOf S2 ) by FUNCT_2:def 1;
then reconsider l2 = l1 as ofAtomicFormula Element of S2 by FOMODEL1:def 20;
l2 in OwnSymbolsOf S2 by A1, FOMODEL1:15;
then reconsider l2 = l2 as own Element of S2 ;
ar l1 = ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1))) . l1 by A11, FUNCT_1:49
.= ar l2 by A6, A11, FUNCT_1:49 ;
then not l2 is low-compounding ;
then reconsider l2 = l2 as literal Element of S2 ;
take phi2 = <*l2*> ^ h2; :: thesis:
phi11 = (<*l2*> ^ h1) ^ (tail phi11) by FOMODEL2:23;
hence phi1 = phi2 by A10; :: thesis:
reconsider l2 = l2 as literal Element of S2 ;

end;

suppose not phi11 is exal ; :: thesis:

then reconsider phi11 = phi11 as non 0wff n + 1 -wff non exal string of S1 ;
reconsider t1 = tail phi11 as n -wff string of S1 ;
reconsider z1 = rng t1 as non empty Subset of (rng phi1) by A8, FINSEQ_1:30;
reconsider z11 = z1 /\ (OwnSymbolsOf S1) as Subset of ((rng phi1) /\ (OwnSymbolsOf S1)) by XBOOLE_1:26;
A12: I1 | (z11 null ((rng phi1) /\ (OwnSymbolsOf S1))) = (I2 | ((rng phi1) /\ (OwnSymbolsOf S1))) | z11 by A6, RELAT_1:71
.= I2 | (z11 null ((rng phi1) /\ (OwnSymbolsOf S1))) by RELAT_1:71 ;
the adicity of S1 | (z11 null ((rng phi1) /\ (OwnSymbolsOf S1))) = ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1))) | z11 by RELAT_1:71
.= the adicity of S2 | (z11 null ((rng phi1) /\ (OwnSymbolsOf S1))) by RELAT_1:71, A6 ;
then consider t2 being n -wff string of S2 such that
A13: t1 = t2 by A5, A12;
take phi2 = (<*(TheNorSymbOf S2)*> ^ h2) ^ t2; :: thesis:
((S1 -firstChar) . phi11) \+\ (TheNorSymbOf S1) = {} ;
hence phi1 = phi2 by A1, A10, A13, A8, FOMODEL0:29; :: thesis:

end;

A14: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
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;
phi1 null 0 is (Depth phi1) + 0 -wff ;
then reconsider phi11 = phi1 as Depth phi1 -wff string of S1 ;
set x1 = rng phi1;
set x11 = (rng phi1) /\ (OwnSymbolsOf S1);
assume ( the adicity of S1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = the adicity of S2 | ((rng phi1) /\ (OwnSymbolsOf S1)) & I1 | ((rng phi1) /\ (OwnSymbolsOf S1)) = I2 | ((rng phi1) /\ (OwnSymbolsOf S1)) ) ; :: thesis:
then consider phi2 being Depth phi1 -wff string of S2 such that
A15: phi2 = phi11 by A14;
take phi2 ; :: thesis:
thus phi1 = phi2 by A15; :: thesis: