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 ) );
A1: S₁[ 0 ] ;
A2: 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 A3: 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);
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 A3, Def20;
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 FUNCT_4:def 1, A8, A5;
hence ((S,U) -TruthEval m) . x = ((S,U) -TruthEval (m + (n + 1))) . x by A3, A4, A7, A5, FUNCT_4:def 1; :: thesis: verum

end;

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