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 S1[ Nat] means F . $1 c= F . ($1 + 1);
A3: 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= F . (n + 1) ; :: thesis: S1[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 S1[n + 1] by A2; :: thesis: verum
end;
let n be Nat; :: thesis: F . n c= F . (n + 1)
F . (0 + 1) = (N . 0) \ (N . 0) by A2;
then A4: S1[ 0 ] by A1, XBOOLE_1:37;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A3);
 hence F . n c= F . (n + 1) ; :: thesis: verum