defpred S1[ Nat] means for F being Function st card (rng F) = \$1 holds
P1[F];
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 A4: S1[n] ; :: thesis: S1[n + 1]
let F be Function; :: thesis: ( card (rng F) = n + 1 implies P1[F] )
assume A5: card (rng F) = n + 1 ; :: thesis: P1[F]
for x being set st x in rng F & P2[x,F] holds
P1[F | ((dom F) \ (F " {x}))]
proof
let x be set ; :: thesis: ( x in rng F & P2[x,F] implies P1[F | ((dom F) \ (F " {x}))] )
assume that
A6: x in rng F and
P2[x,F] ; :: thesis: P1[F | ((dom F) \ (F " {x}))]
set D = (dom F) \ (F " {x});
card ((rng F) \ {x}) = n by A5, A6, Th55;
then card (rng (F | ((dom F) \ (F " {x})))) = n by Th54;
hence P1[F | ((dom F) \ (F " {x}))] by A4; :: thesis: verum
end;
hence P1[F] by A2; :: thesis: verum
end;
let F be Function; :: thesis: ( rng F is finite implies P1[F] )
assume rng F is finite ; :: thesis: P1[F]
then reconsider n = card (rng F) as Nat ;
A7: card (rng F) = n ;
A8: S1[ 0 ]
proof
let F be Function; :: thesis: ( card (rng F) = 0 implies P1[F] )
assume card (rng F) = 0 ; :: thesis: P1[F]
then rng F = {} ;
hence P1[F] by A1, RELAT_1:41; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A8, A3);
hence P1[F] by A7; :: thesis: verum