let U be non empty set ; :: thesis: for S1, S2 being Language st TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 holds

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

let S1, S2 be Language; :: thesis: ( TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 implies for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2 )

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: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

defpred S_{1}[ 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_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A2, A4);

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 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 wff string of S2 st phi1 = phi2

let phi1 be wff string of S1; :: thesis: ( 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)) implies ex phi2 being wff string of S2 st phi1 = phi2 )

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: ex phi2 being wff string of S2 st phi1 = phi2

then consider phi2 being Depth phi1 -wff string of S2 such that

A15: phi2 = phi11 by A14;

take phi2 ; :: thesis: phi1 = phi2

thus phi1 = phi2 by A15; :: thesis: verum

for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

let S1, S2 be Language; :: thesis: ( TheEqSymbOf S1 = TheEqSymbOf S2 & TheNorSymbOf S1 = TheNorSymbOf S2 implies for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2 )

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: for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

defpred S

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

proof

A4:
for n being Nat st S
let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2

for phi1 being 0 -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 0 -wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 0 -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 0 -wff string of S2 st phi1 = phi2

let phi1 be 0 -wff string of S1; :: thesis: ( 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)) implies ex phi2 being 0 -wff string of S2 st phi1 = phi2 )

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: ex phi2 being 0 -wff string of S2 st phi1 = phi2

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: verum

end;for phi1 being 0 -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 0 -wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 0 -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 0 -wff string of S2 st phi1 = phi2

let phi1 be 0 -wff string of S1; :: thesis: ( 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)) implies ex phi2 being 0 -wff string of S2 st phi1 = phi2 )

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: ex phi2 being 0 -wff string of S2 st phi1 = phi2

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: verum

S

proof

A14:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set N = n + 1;

assume A5: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2

for phi1 being n + 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 n + 1 -wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being n + 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 n + 1 -wff string of S2 st phi1 = phi2

let phi1 be n + 1 -wff string of S1; :: thesis: ( 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)) implies ex phi2 being n + 1 -wff string of S2 st phi1 = phi2 )

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: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

end;set N = n + 1;

assume A5: S

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2

for phi1 being n + 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 n + 1 -wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being n + 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 n + 1 -wff string of S2 st phi1 = phi2

let phi1 be n + 1 -wff string of S1; :: thesis: ( 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)) implies ex phi2 being n + 1 -wff string of S2 st phi1 = phi2 )

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: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

per cases
( phi1 is 0wff or not phi1 is 0wff )
;

end;

suppose
phi1 is 0wff
; :: thesis: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

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: phi1 = phi22

thus phi1 = phi22 by A7; :: thesis: verum

end;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: phi1 = phi22

thus phi1 = phi22 by A7; :: thesis: verum

suppose
not phi1 is 0wff
; :: thesis: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

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;

end;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
( phi11 is exal or not phi11 is exal )
;

end;

suppose
phi11 is exal
; :: thesis: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

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: phi1 = phi2

phi11 = (<*l2*> ^ h1) ^ (tail phi11) by FOMODEL2:23;

hence phi1 = phi2 by A10; :: thesis: verum

reconsider l2 = l2 as literal Element of S2 ;

end;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: phi1 = phi2

phi11 = (<*l2*> ^ h1) ^ (tail phi11) by FOMODEL2:23;

hence phi1 = phi2 by A10; :: thesis: verum

reconsider l2 = l2 as literal Element of S2 ;

suppose
not phi11 is exal
; :: thesis: ex phi2 being n + 1 -wff string of S2 st phi1 = phi2

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: phi1 = phi2

((S1 -firstChar) . phi11) \+\ (TheNorSymbOf S1) = {} ;

hence phi1 = phi2 by A1, A10, A13, A8, FOMODEL0:29; :: thesis: verum

end;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: phi1 = phi2

((S1 -firstChar) . phi11) \+\ (TheNorSymbOf S1) = {} ;

hence phi1 = phi2 by A1, A10, A13, A8, FOMODEL0:29; :: thesis: verum

let I1 be Element of U -InterpretersOf S1; :: thesis: for I2 being Element of U -InterpretersOf S2

for phi1 being 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 wff string of S2 st phi1 = phi2

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 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 wff string of S2 st phi1 = phi2

let phi1 be wff string of S1; :: thesis: ( 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)) implies ex phi2 being wff string of S2 st phi1 = phi2 )

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: ex phi2 being wff string of S2 st phi1 = phi2

then consider phi2 being Depth phi1 -wff string of S2 such that

A15: phi2 = phi11 by A14;

take phi2 ; :: thesis: phi1 = phi2

thus phi1 = phi2 by A15; :: thesis: verum