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 S1[ 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: S1[ 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 ([:(),((() *) \ ):],BOOLEAN) ;
reconsider g2 = ((S,U2) -TruthEval) . Z as Element of PFuncs ([:(),((() *) \ ):],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) = [:(),():] by ;
A5: dom ((S,U2) -TruthEval 0) = [:(),():] by ;
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 ;
hence [I2,w] in dom ((S,U2) -TruthEval 0) by ; :: thesis: verum
end;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume A7: S1[n] ; :: thesis: S1[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 ([:(),((() *) \ ):],BOOLEAN) ;
reconsider g1n = ((S,U1) -TruthEval) . nn as Element of PFuncs ([:(),((() *) \ ):],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 ([:(),((() *) \ ):],BOOLEAN) ;
reconsider g2n = ((S,U2) -TruthEval) . nn as Element of PFuncs ([:(),((() *) \ ):],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 ;
then [I2,w] in dom (ExIterator ((S,U2) -TruthEval n)) by Def16;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by ; :: 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 = (<*()*> ^ phi1) ^ phi2 & [I1,phi1] in dom ((S,U1) -TruthEval n) & [I1,phi2] in dom ((S,U1) -TruthEval n) ) by Def18;
( w = (<*()*> ^ phi1) ^ phi2 & [I2,phi1] in dom ((S,U2) -TruthEval n) & [I2,phi2] in dom ((S,U2) -TruthEval n) ) by ;
then [I2,w] in dom (NorIterator ((S,U2) -TruthEval n)) by Def18;
hence [I2,w] in dom ((S,U2) -TruthEval (n + 1)) by ; :: 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 ; :: thesis: verum
end;
end;
end;
thus for m being Nat holds S1[m] from NAT_1:sch 2(A1, A6); :: thesis: verum