let m be Nat; :: thesis: for x being set
for S being Language
for U being non empty set
for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
let x be set ; :: thesis: for S being Language
for U being non empty set
for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
let S be Language; :: thesis: for U being non empty set
for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
let U be non empty set ; :: thesis: for n being Nat st x in dom ((S,U) -TruthEval m) holds
( x in dom ((S,U) -TruthEval (m + n)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + n)) . x )
set f = (S,U) -TruthEval ;
defpred S₁[ Nat] means ( x in dom ((S,U) -TruthEval m) implies ( x in dom ((S,U) -TruthEval (m + $1)) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + $1)) . x ) );
B0: S₁[ 0 ] ;
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 k = m + n, K = (m + n) + 1 as Element of NAT by ORDINAL1:def 12;
assume C1: S₁[n] ; :: thesis: S₁[n + 1]
set g = (S,U) -TruthEval m;
set g0 = (S,U) -TruthEval (m + n);
set g1 = (S,U) -TruthEval ((m + n) + 1);
C2: ( ((S,U) -TruthEval) . k = (S,U) -TruthEval (m + n) & ((S,U) -TruthEval) . K = (S,U) -TruthEval ((m + n) + 1) ) by DefTruth2;
C6: ((S,U) -TruthEval) . K = ((ExIterator (((S,U) -TruthEval) . k)) +* (NorIterator (((S,U) -TruthEval) . k))) +* (((S,U) -TruthEval) . k) by DefTruth1;
then dom (((S,U) -TruthEval) . K) = (dom ((ExIterator (((S,U) -TruthEval) . k)) +* (NorIterator (((S,U) -TruthEval) . k)))) \/ (dom (((S,U) -TruthEval) . k)) by FUNCT_4:def 1;
then C3: dom (((S,U) -TruthEval) . k) c= dom (((S,U) -TruthEval) . K) by XBOOLE_1:7;
assume C8: x in dom ((S,U) -TruthEval m) ; :: thesis: ( x in dom ((S,U) -TruthEval (m + (n + 1))) & ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + (n + 1))) . x )
then x in dom (((S,U) -TruthEval) . k) by C1, DefTruth2;
then C5: x in dom (((S,U) -TruthEval) . K) by C3;
thus x in dom ((S,U) -TruthEval (m + (n + 1))) by C2, C8, C1, C3; :: thesis: ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + (n + 1))) . x
x in (dom ((ExIterator (((S,U) -TruthEval) . k)) +* (NorIterator (((S,U) -TruthEval) . k)))) \/ (dom (((S,U) -TruthEval) . k)) by C5, C6, FUNCT_4:def 1;
hence ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + (n + 1))) . x by C1, C2, C8, C6, FUNCT_4:def 1; :: thesis: verum

end;

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