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);
B0: 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) ;
D1: ( (S,U1) -TruthEval 0 = g1 & (S,U2) -TruthEval 0 = g2 ) by DefTruth2;
D2: ( g1 = S -TruthEval U1 & g2 = S -TruthEval U2 ) by DefTruth1;
D3: dom ((S,U1) -TruthEval 0) = [:(U1 -InterpretersOf S),(AtomicFormulasOf S):] by D1, D2, FUNCT_2:def 1;
D4: dom ((S,U2) -TruthEval 0) = [:(U2 -InterpretersOf S),(AtomicFormulasOf S):] by D1, D2, FUNCT_2:def 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 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 D3, ZFMISC_1:87;
hence [I2,w] in dom ((S,U2) -TruthEval 0) by D4, ZFMISC_1:87; :: thesis: verum

end;

B1: 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 C0: 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);
C11: 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) ;
D1: ( (S,U1) -TruthEval n = g1n & (S,U1) -TruthEval (n + 1) = g1N ) by DefTruth2;
then (S,U1) -TruthEval (n + 1) = ((ExIterator g1n) +* (NorIterator g1n)) +* g1n by DefTruth1;
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 D1; :: thesis: verum

end;

C12: 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) ;
D1: ( (S,U2) -TruthEval n = g2n & (S,U2) -TruthEval (n + 1) = g2N ) by DefTruth2;
then (S,U2) -TruthEval (n + 1) = ((ExIterator g2n) +* (NorIterator g2n)) +* g2n by DefTruth1;
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 D1; :: 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 Z0: [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 Z0, Lm25, C11;

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
D1: ( [I1,ww] in dom ((S,U1) -TruthEval n) & w = <*v*> ^ ww ) by DefExIter;
( [I2,ww] in dom ((S,U2) -TruthEval n) & w = <*v*> ^ ww ) by D1, C0;
then [I2,w] in dom (ExIterator ((S,U2) -TruthEval n)) by DefExIter;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm25, C12; :: 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
D1: ( w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [I1,phi1] in dom ((S,U1) -TruthEval n) & [I1,phi2] in dom ((S,U1) -TruthEval n) ) by DefNorIter;
( w = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & [I2,phi1] in dom ((S,U2) -TruthEval n) & [I2,phi2] in dom ((S,U2) -TruthEval n) ) by D1, C0;
then [I2,w] in dom (NorIterator ((S,U2) -TruthEval n)) by DefNorIter;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm25, C12; :: 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 C0;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by Lm25, C12; :: thesis: verum

end;

end;

end;

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