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 S1[ 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 ) );
A1: S1[ 0 ] ;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
reconsider k = m + n, K = (m + n) + 1 as Element of NAT by ORDINAL1:def 12;
assume A3: S1[n] ; :: thesis: S1[n + 1]
set g = (S,U) -TruthEval m;
set g0 = (S,U) -TruthEval (m + n);
set g1 = (S,U) -TruthEval ((m + n) + 1);
A4: ( ((S,U) -TruthEval) . k = (S,U) -TruthEval (m + n) & ((S,U) -TruthEval) . K = (S,U) -TruthEval ((m + n) + 1) ) by Def20;
A5: ((S,U) -TruthEval) . K = ((ExIterator (((S,U) -TruthEval) . k)) +* (NorIterator (((S,U) -TruthEval) . k))) +* (((S,U) -TruthEval) . k) by Def19;
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 A6: dom (((S,U) -TruthEval) . k) c= dom (((S,U) -TruthEval) . K) by XBOOLE_1:7;
assume A7: 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 ;
then A8: x in dom (((S,U) -TruthEval) . K) by A6;
thus x in dom ((S,U) -TruthEval (m + (n + 1))) by A4, A7, A3, A6; :: 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 ;
hence ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + (n + 1))) . x by ; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2); :: thesis: verum