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

F . n c= N . m

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

( 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

A8:
for n, m being Nat st n <= m holds
defpred S_{1}[ Nat] means F . $1 c= N . $1;

A6: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by A1;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A7, A6); :: thesis: verum

end;A6: for n being Nat st S

S

proof

A7:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume F . n c= N . n ; :: thesis: S_{1}[n + 1]

F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume F . n c= N . n ; :: thesis: S

F . (n + 1) = (N . (n + 1)) \ (N . n) by A2;

hence S

thus for n being Nat holds S

F . n c= N . m

proof

reconsider k = k as Element of NAT by ORDINAL1:def 12;
let n, m be Nat; :: thesis: ( n <= m implies F . n c= N . m )

A9: ( n < m implies 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;A9: ( n < m implies F . n c= N . m )

proof

assume
n <= m
; :: thesis: F . n c= N . m
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;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

then ( n = m or n < m ) by XXREAL_0:1;

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

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