let N be Subset of NAT; :: thesis: ( N is finite implies ex k being Nat st

for n being Nat st n in N holds

n <= k )

assume N is finite ; :: thesis: ex k being Nat st

for n being Nat st n in N holds

n <= k

then reconsider n = card N as Nat ;

A1: N,n are_equipotent by CARD_1:def 2;

consider F being Function such that

F is one-to-one and

A2: dom F = n and

A3: rng F = N by A1, WELLORD2:def 4;

reconsider F = F as XFinSequence by A2, AFINSQ_1:5;

reconsider F = F as XFinSequence of NAT by A3, RELAT_1:def 19;

reconsider k = Sum F as Element of NAT by ORDINAL1:def 12;

take k ; :: thesis: for n being Nat st n in N holds

n <= k

let n be Nat; :: thesis: ( n in N implies n <= k )

assume A4: n in N ; :: thesis: n <= k

F <> 0 by A3, A4;

then A5: len F > 0 ;

ex x being object st

( x in dom F & F . x = n ) by A3, A4, FUNCT_1:def 3;

hence n <= k by A5, AFINSQ_2:61; :: thesis: verum

for n being Nat st n in N holds

n <= k )

assume N is finite ; :: thesis: ex k being Nat st

for n being Nat st n in N holds

n <= k

then reconsider n = card N as Nat ;

A1: N,n are_equipotent by CARD_1:def 2;

consider F being Function such that

F is one-to-one and

A2: dom F = n and

A3: rng F = N by A1, WELLORD2:def 4;

reconsider F = F as XFinSequence by A2, AFINSQ_1:5;

reconsider F = F as XFinSequence of NAT by A3, RELAT_1:def 19;

reconsider k = Sum F as Element of NAT by ORDINAL1:def 12;

take k ; :: thesis: for n being Nat st n in N holds

n <= k

let n be Nat; :: thesis: ( n in N implies n <= k )

assume A4: n in N ; :: thesis: n <= k

F <> 0 by A3, A4;

then A5: len F > 0 ;

ex x being object st

( x in dom F & F . x = n ) by A3, A4, FUNCT_1:def 3;

hence n <= k by A5, AFINSQ_2:61; :: thesis: verum