let S be Language; :: thesis: for U1, U2 being non empty set
for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
let U1, U2 be non empty set ; :: thesis: for m being Nat
for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval m) holds
[I2,w] in dom ((S,U2) -TruthEval m)
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set II1 = U1 -InterpretersOf S;
set II2 = U2 -InterpretersOf S;
set AF = AtomicFormulasOf S;
defpred S₁[ Nat] means for I1 being Element of U1 -InterpretersOf S
for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval $1) holds
[I2,w] in dom ((S,U2) -TruthEval $1);
A1: S₁[ 0 ]

proof

set f1 = (S,U1) -TruthEval 0;
set f2 = (S,U2) -TruthEval 0;
reconsider Z = 0 as Element of NAT ;
reconsider g1 = ((S,U1) -TruthEval) . Z as Element of PFuncs ([:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
reconsider g2 = ((S,U2) -TruthEval) . Z as Element of PFuncs ([:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
A2: ( (S,U1) -TruthEval 0 = g1 & (S,U2) -TruthEval 0 = g2 ) by Def20;
A3: ( g1 = S -TruthEval U1 & g2 = S -TruthEval U2 ) by Def19;
A4: dom ((S,U1) -TruthEval 0) = [:(U1 -InterpretersOf S),(AtomicFormulasOf S):] by A2, FUNCT_2:def 1, A3;
A5: dom ((S,U2) -TruthEval 0) = [:(U2 -InterpretersOf S),(AtomicFormulasOf S):] by A2, FUNCT_2:def 1, A3;
let I1 be Element of U1 -InterpretersOf S; :: thesis: for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval 0) holds
[I2,w] in dom ((S,U2) -TruthEval 0)
let I2 be Element of U2 -InterpretersOf S; :: thesis: for w being string of S st [I1,w] in dom ((S,U1) -TruthEval 0) holds
[I2,w] in dom ((S,U2) -TruthEval 0)
let w be string of S; :: thesis: ( [I1,w] in dom ((S,U1) -TruthEval 0) implies [I2,w] in dom ((S,U2) -TruthEval 0) )
assume [I1,w] in dom ((S,U1) -TruthEval 0) ; :: thesis: [I2,w] in dom ((S,U2) -TruthEval 0)
then ( I1 in U1 -InterpretersOf S & w in AtomicFormulasOf S ) by ZFMISC_1:87, A4;
hence [I2,w] in dom ((S,U2) -TruthEval 0) by A5, ZFMISC_1:87; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
let I1 be Element of U1 -InterpretersOf S; :: thesis: for I2 being Element of U2 -InterpretersOf S
for w being string of S st [I1,w] in dom ((S,U1) -TruthEval (n + 1)) holds
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
let I2 be Element of U2 -InterpretersOf S; :: thesis: for w being string of S st [I1,w] in dom ((S,U1) -TruthEval (n + 1)) holds
[I2,w] in dom ((S,U2) -TruthEval (n + 1))
set f1n = (S,U1) -TruthEval n;
set f1N = (S,U1) -TruthEval (n + 1);
set f2n = (S,U2) -TruthEval n;
set f2N = (S,U2) -TruthEval (n + 1);
A8: dom ((S,U1) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U1) -TruthEval n))) \/ (dom (NorIterator ((S,U1) -TruthEval n)))) \/ (dom ((S,U1) -TruthEval n))

proof

reconsider g1N = ((S,U1) -TruthEval) . NN as Element of PFuncs ([:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
reconsider g1n = ((S,U1) -TruthEval) . nn as Element of PFuncs ([:(U1 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
A9: ( (S,U1) -TruthEval n = g1n & (S,U1) -TruthEval (n + 1) = g1N ) by Def20;
then (S,U1) -TruthEval (n + 1) = ((ExIterator g1n) +* (NorIterator g1n)) +* g1n by Def19;
then dom ((S,U1) -TruthEval (n + 1)) = (dom ((ExIterator g1n) +* (NorIterator g1n))) \/ (dom g1n) by FUNCT_4:def 1
.= ((dom (ExIterator g1n)) \/ (dom (NorIterator g1n))) \/ (dom g1n) by FUNCT_4:def 1 ;
hence dom ((S,U1) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U1) -TruthEval n))) \/ (dom (NorIterator ((S,U1) -TruthEval n)))) \/ (dom ((S,U1) -TruthEval n)) by A9; :: thesis: verum

end;

A10: dom ((S,U2) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U2) -TruthEval n))) \/ (dom (NorIterator ((S,U2) -TruthEval n)))) \/ (dom ((S,U2) -TruthEval n))

proof

reconsider g2N = ((S,U2) -TruthEval) . NN as Element of PFuncs ([:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
reconsider g2n = ((S,U2) -TruthEval) . nn as Element of PFuncs ([:(U2 -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN) ;
A11: ( (S,U2) -TruthEval n = g2n & (S,U2) -TruthEval (n + 1) = g2N ) by Def20;
then (S,U2) -TruthEval (n + 1) = ((ExIterator g2n) +* (NorIterator g2n)) +* g2n by Def19;
then dom ((S,U2) -TruthEval (n + 1)) = (dom ((ExIterator g2n) +* (NorIterator g2n))) \/ (dom g2n) by FUNCT_4:def 1
.= ((dom (ExIterator g2n)) \/ (dom (NorIterator g2n))) \/ (dom g2n) by FUNCT_4:def 1 ;
hence dom ((S,U2) -TruthEval (n + 1)) = ((dom (ExIterator ((S,U2) -TruthEval n))) \/ (dom (NorIterator ((S,U2) -TruthEval n)))) \/ (dom ((S,U2) -TruthEval n)) by A11; :: thesis: verum

end;

let w be string of S; :: thesis: ( [I1,w] in dom ((S,U1) -TruthEval (n + 1)) implies [I2,w] in dom ((S,U2) -TruthEval (n + 1)) )
set x = [I1,w];
assume A12: [I1,w] in dom ((S,U1) -TruthEval (n + 1)) ; :: thesis: [I2,w] in dom ((S,U2) -TruthEval (n + 1))

per cases ( [I1,w] in dom (ExIterator ((S,U1) -TruthEval n)) or [I1,w] in dom (NorIterator ((S,U1) -TruthEval n)) or [I1,w] in dom ((S,U1) -TruthEval n) ) by A12, Lm8, A8;

suppose [I1,w] in dom (ExIterator ((S,U1) -TruthEval n)) ; :: thesis: [I2,w] in dom ((S,U2) -TruthEval (n + 1))

then consider v being literal Element of S, ww being string of S such that
A13: ( [I1,ww] in dom ((S,U1) -TruthEval n) & w = <*v*> ^ ww ) by Def16;
( [I2,ww] in dom ((S,U2) -TruthEval n) & w = <*v*> ^ ww ) by A13, A7;
then [I2,w] in dom (ExIterator ((S,U2) -TruthEval n)) by Def16;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm8, A10; :: thesis: verum

end;

suppose [I1,w] in dom (NorIterator ((S,U1) -TruthEval n)) ; :: thesis: [I2,w] in dom ((S,U2) -TruthEval (n + 1))

then consider phi1, phi2 being string of S such that
A14: ( w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [I1,phi1] in dom ((S,U1) -TruthEval n) & [I1,phi2] in dom ((S,U1) -TruthEval n) ) by Def18;
( w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [I2,phi1] in dom ((S,U2) -TruthEval n) & [I2,phi2] in dom ((S,U2) -TruthEval n) ) by A14, A7;
then [I2,w] in dom (NorIterator ((S,U2) -TruthEval n)) by Def18;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm8, A10; :: thesis: verum

end;

suppose [I1,w] in dom ((S,U1) -TruthEval n) ; :: thesis: [I2,w] in dom ((S,U2) -TruthEval (n + 1))

then [I2,w] in dom ((S,U2) -TruthEval n) by A7;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm8, A10; :: thesis: verum

end;

end;

end;

thus for m being Nat holds S₁[m] from NAT_1:sch 2(A1, A6); :: thesis: verum