defpred S₁[ Element of NAT ] means for F being Function st card (rng F) = $1 holds
P₁[F];
A3: S₁[ 0 ]

proof

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

end;

A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let F be Function; :: thesis: ( card (rng F) = n + 1 implies P₁[F] )
assume A7: 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 A8: ( x in rng F & P₂[x,F] ) ; :: thesis: P₁[F | ((dom F) \ (F " {x}))]
set D = (dom F) \ (F " {x});
card ((rng F) \ {x}) = n by A7, A8, Th65;
then card (rng (F | ((dom F) \ (F " {x})))) = n by Th64;
hence P₁[F | ((dom F) \ (F " {x}))] by A6; :: thesis: verum

end;

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

end;

let F be Function; :: thesis: ( rng F is finite implies P₁[F] )
assume A9: rng F is finite ; :: thesis: P₁[F]
consider n being Nat such that
A10: rng F,n are_equipotent by A9, CARD_1:74;
A11: n in NAT by ORDINAL1:def 13;
A12: card (rng F) = n by A10, CARD_1:def 5;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A5);
hence P₁[F] by A11, A12; :: thesis: verum