let N, F be Function; :: thesis: ( F . 0 = {} & ( for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies for n being Nat holds F . n c= F . (n + 1) )

assume that

A1: F . 0 = {} and

A2: for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ; :: thesis: for n being Nat holds F . n c= F . (n + 1)

defpred S_{1}[ Nat] means F . $1 c= F . ($1 + 1);

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

S_{1}[n + 1]

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

then A4: S_{1}[ 0 ]
by A1, XBOOLE_1:37;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A3);

hence F . n c= F . (n + 1) ; :: thesis: verum

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies for n being Nat holds F . n c= F . (n + 1) )

assume that

A1: F . 0 = {} and

A2: for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ; :: thesis: for n being Nat holds F . n c= F . (n + 1)

defpred S

A3: for n being Nat st S

S

proof

let n be Nat; :: thesis: F . n c= F . (n + 1)
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

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

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

then (N . 0) \ (N . n) c= F . ((n + 1) + 1) by A2, XBOOLE_1:34;

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

end;assume F . n c= F . (n + 1) ; :: thesis: S

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

then (N . 0) \ (N . n) c= F . ((n + 1) + 1) by A2, XBOOLE_1:34;

hence S

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

then A4: S

for n being Nat holds S

hence F . n c= F . (n + 1) ; :: thesis: verum