let U be non empty set ; :: thesis: for S1, S2 being Language st TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let S1, S2 be Language; :: thesis: ( TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

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: ( not TheEqSymbOf S1 = TheEqSymbOf S2 or not the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) or for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

assume A2: ( TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) ) ; :: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

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

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

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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let phi1 be wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

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

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

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: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let S1, S2 be Language; :: thesis: ( TheNorSymbOf S1 = TheNorSymbOf S2 & TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

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: ( not TheEqSymbOf S1 = TheEqSymbOf S2 or not the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) or for I1 being Element of U -InterpretersOf S1

for I2 being Element of U -InterpretersOf S2

for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

assume A2: ( TheEqSymbOf S1 = TheEqSymbOf S2 & the adicity of S1 | (OwnSymbolsOf S1) = the adicity of S2 | (OwnSymbolsOf S1) ) ; :: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

defpred S

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

proof

A6:
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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 0 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let phi1 be 0 -wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) )

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

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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

end;for phi1 being 0 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being 0 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let phi1 be 0 -wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being 0 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) )

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

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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

S

proof

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

assume A7: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being n + 1 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let phi1 be n + 1 -wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) )

set X = rng phi1;

assume A8: I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ; :: thesis: ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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;

end;assume A7: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being n + 1 -wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

let phi1 be n + 1 -wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 ) )

set X = rng phi1;

assume A8: I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) ; :: thesis: ex phi2 being n + 1 -wff string of S2 st

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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;

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

end;

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

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

A11: phi1 = (<*l1*> ^ h1) ^ (tail phi11) by FOMODEL2:23

.= <*l1*> ^ h1 ;

hence phi1 = phi2 by A9; :: thesis: I1 -TruthEval phi1 = I2 -TruthEval phi2

( I1 -TruthEval phi11 = 1 iff I2 -TruthEval phi2 = 1 )

hence I1 -TruthEval phi1 = I2 -TruthEval phi2 by FOMODEL0:39; :: thesis: verum

end;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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

A11: phi1 = (<*l1*> ^ h1) ^ (tail phi11) by FOMODEL2:23

.= <*l1*> ^ h1 ;

hence phi1 = phi2 by A9; :: thesis: I1 -TruthEval phi1 = I2 -TruthEval phi2

( I1 -TruthEval phi11 = 1 iff I2 -TruthEval phi2 = 1 )

proof

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

end;

then
( I1 -TruthEval phi1 = 1 iff not I2 -TruthEval phi2 = 0 )
by FOMODEL0:39;hereby :: thesis: ( I2 -TruthEval phi2 = 1 implies I1 -TruthEval phi11 = 1 )

assume
I2 -TruthEval phi2 = 1
; :: thesis: I1 -TruthEval phi11 = 1assume
I1 -TruthEval phi11 = 1
; :: thesis: I2 -TruthEval phi2 = 1

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

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

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

hence I1 -TruthEval phi1 = I2 -TruthEval phi2 by FOMODEL0:39; :: thesis: verum

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

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

( ((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: I1 -TruthEval phi1 = I2 -TruthEval phi2

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

end;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: ( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

( ((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: I1 -TruthEval phi1 = I2 -TruthEval phi2

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

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

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

( phi1 = phi2 & I1 -TruthEval phi1 = I2 -TruthEval phi2 )

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: ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 )

thus ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by A18; :: thesis: verum

end;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: ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 )

thus ( phi1 = phi22 & I1 -TruthEval phi1 = I2 -TruthEval phi22 ) by A18; :: 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 I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let I2 be Element of U -InterpretersOf S2; :: thesis: for phi1 being wff string of S1 st I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) holds

ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

let phi1 be wff string of S1; :: thesis: ( I1 | (OwnSymbolsOf S1) = I2 | (OwnSymbolsOf S1) implies ex phi2 being wff string of S2 st

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 ) )

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

( phi2 = phi1 & I2 -TruthEval phi2 = I1 -TruthEval phi1 )

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