let m be Nat; 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 ; 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; 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 ; 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;
( 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]
;
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)
;
( 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;
((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;
verum
end;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2); verum