let N, F be Function; :: thesis: ( F . 0 = N . 0 & ( for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies for n, m being Nat st n < m holds
F . n misses F . m )
assume that
A1: F . 0 = N . 0 and
A2: for n being Nat holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; :: thesis: for n, m being Nat st n < m holds
F . n misses F . m
let n, m be Nat; :: thesis: ( n < m implies F . n misses F . m )
assume A3: n < m ; :: thesis: F . n misses F . m
then 0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
A5: for n being Nat holds F . n c= N . n
proof
defpred S1[ Nat] means F . $1 c= N . $1;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume F . n c= N . n ; :: thesis: S1[n + 1]
F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;
hence S1[n + 1] ; :: thesis: verum
end;
A7: S1[ 0 ] by A1;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A7, A6); :: thesis: verum
end;
A8: for n, m being Nat st n <= m holds
F . n c= N . m
proof
let n, m be Nat; :: thesis: ( n <= m implies F . n c= N . m )
A9: ( n < m implies F . n c= N . m )
proof
assume n < m ; :: thesis: F . n c= N . m
then A10: N . n c= N . m by A2, Th18;
F . n c= N . n by A5;
hence F . n c= N . m by A10; :: thesis: verum
end;
assume n <= m ; :: thesis: F . n c= N . m
then ( n = m or n < m ) by XXREAL_0:1;
hence F . n c= N . m by A5, A9; :: thesis: verum
end;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
F . (k + 1) = (N . (k + 1)) \ (N . k) by A2;
then A11: N . k misses F . (k + 1) by XBOOLE_1:79;
n <= k by A3, A4, NAT_1:13;
then (F . n) /\ (F . (k + 1)) = ((F . n) /\ (N . k)) /\ (F . (k + 1)) by A8, XBOOLE_1:28
.= (F . n) /\ ((N . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A11
.= {} ;
hence F . n misses F . m by A4; :: thesis: verum