defpred S_{1}[ Nat] means for F being Function st card (rng F) = $1 holds

P_{1}[F];

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[F] )

assume rng F is finite ; :: thesis: P_{1}[F]

then reconsider n = card (rng F) as Nat ;

A7: card (rng F) = n ;

A8: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A8, A3);

hence P_{1}[F]
by A7; :: thesis: verum

P

A3: for n being Nat st S

S

proof

let F be Function; :: thesis: ( rng F is finite implies P
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let F be Function; :: thesis: ( card (rng F) = n + 1 implies P_{1}[F] )

assume A5: card (rng F) = n + 1 ; :: thesis: P_{1}[F]

for x being set st x in rng F & P_{2}[x,F] holds

P_{1}[F | ((dom F) \ (F " {x}))]
_{1}[F]
by A2; :: thesis: verum

end;assume A4: S

let F be Function; :: thesis: ( card (rng F) = n + 1 implies P

assume A5: card (rng F) = n + 1 ; :: thesis: P

for x being set st x in rng F & P

P

proof

hence
P
let x be set ; :: thesis: ( x in rng F & P_{2}[x,F] implies P_{1}[F | ((dom F) \ (F " {x}))] )

assume that

A6: x in rng F and

P_{2}[x,F]
; :: thesis: P_{1}[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_{1}[F | ((dom F) \ (F " {x}))]
by A4; :: thesis: verum

end;assume that

A6: x in rng F and

P

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

assume rng F is finite ; :: thesis: P

then reconsider n = card (rng F) as Nat ;

A7: card (rng F) = n ;

A8: S

proof

for k being Nat holds S
let F be Function; :: thesis: ( card (rng F) = 0 implies P_{1}[F] )

assume card (rng F) = 0 ; :: thesis: P_{1}[F]

then rng F = {} ;

hence P_{1}[F]
by A1, RELAT_1:41; :: thesis: verum

end;assume card (rng F) = 0 ; :: thesis: P

then rng F = {} ;

hence P

hence P