defpred S₁[ Nat] means for F being Function st card (rng F) = $1 holds
P₁[F];
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 A4: S₁[n] ; :: thesis: S₁[n + 1]
let F be Function; :: thesis: ( card (rng F) = n + 1 implies P₁[F] )
assume A5: card (rng F) = n + 1 ; :: thesis: P₁[F]
for x being set st x in rng F & P₂[x,F] holds
P₁[F | ((dom F) \ (F " {x}))]

proof

let x be set ; :: thesis: ( x in rng F & P₂[x,F] implies P₁[F | ((dom F) \ (F " {x}))] )
assume that
A6: x in rng F and
P₂[x,F] ; :: thesis: P₁[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 P₁[F | ((dom F) \ (F " {x}))] by A4; :: thesis: verum

end;

hence P₁[F] by A2; :: thesis: verum

end;

let F be Function; :: thesis: ( rng F is finite implies P₁[F] )
assume rng F is finite ; :: thesis: P₁[F]
then reconsider n = card (rng F) as Nat ;
A7: card (rng F) = n ;
A8: S₁[ 0 ]

proof

let F be Function; :: thesis: ( card (rng F) = 0 implies P₁[F] )
assume card (rng F) = 0 ; :: thesis: P₁[F]
then rng F = {} ;
hence P₁[F] by A1, RELAT_1:41; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A3);
hence P₁[F] by A7; :: thesis: verum