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₁[ Nat] means F . $1 c= F . ($1 + 1);
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume F . n c= F . (n + 1) ; :: thesis: S₁[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₁[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: S₁[ 0 ] by A1, XBOOLE_1:37;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A3);
hence F . n c= F . (n + 1) ; :: thesis: verum