let N, F be Function; :: thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) implies for n, m being Element of NAT st n < m holds
F . n misses F . m )
assume A1: ( F . 0 = N . 0 & ( for n being Element of NAT holds
( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) ) ; :: thesis: for n, m being Element of NAT st n < m holds
F . n misses F . m
let n, m be Element of NAT ; :: thesis: ( n < m implies F . n misses F . m )
assume A2: n < m ; :: thesis: F . n misses F . m
then ( 0 <= m & 0 <> m ) by NAT_1:2;
then consider k being Nat such that
A3: m = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
F . (k + 1) = (N . (k + 1)) \ (N . k) by A1;
then A4: N . k misses F . (k + 1) by XBOOLE_1:79;
A5: n <= k by A2, A3, NAT_1:13;
F . n c= N . k

proof

A6: for n being Element of NAT holds F . n c= N . n

proof

defpred S₁[ Element of NAT ] means F . $1 c= N . $1;
A7: S₁[ 0 ] by A1;
A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume F . n c= N . n ; :: thesis: S₁[n + 1]
F . (n + 1) = (N . (n + 1)) \ (N . n) by A1;
hence S₁[n + 1] ; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A8); :: thesis: verum

end;

for n, m being Element of NAT st n <= m holds
F . n c= N . m

proof

let n, m be Element of NAT ; :: thesis: ( n <= m implies F . n c= N . m )
assume n <= m ; :: thesis: F . n c= N . m
then A9: ( n = m or n < m ) by XXREAL_0:1;
( n < m implies F . n c= N . m )

proof

assume A10: n < m ; :: thesis: F . n c= N . m
A11: F . n c= N . n by A6;
N . n c= N . m by A1, A10, Th22;
hence F . n c= N . m by A11, XBOOLE_1:1; :: thesis: verum

end;

hence F . n c= N . m by A6, A9; :: thesis: verum

end;

hence F . n c= N . k by A5; :: thesis: verum

end;

then (F . n) /\ (F . (k + 1)) = ((F . n) /\ (N . k)) /\ (F . (k + 1)) by XBOOLE_1:28
.= (F . n) /\ ((N . k) /\ (F . (k + 1))) by XBOOLE_1:16
.= (F . n) /\ {} by A4, XBOOLE_0:def 7
.= {} ;
hence F . n misses F . m by A3, XBOOLE_0:def 7; :: thesis: verum