let m be Element of NAT ; :: thesis: for X being finite set st card X = m holds

ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

defpred S_{1}[ Nat] means for X being finite set st card X = $1 holds

ex fp being FinSequence st

( len fp = $1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one );

let X be finite set ; :: thesis: ( card X = m implies ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

A1: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
_{1}[m]
from NAT_1:sch 2(A24, A1);

hence ( card X = m implies ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) ) ; :: thesis: verum

ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

defpred S

ex fp being FinSequence st

( len fp = $1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one );

let X be finite set ; :: thesis: ( card X = m implies ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

A1: for m being Nat st S

S

proof

A24:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A2: S_{1}[m]
; :: thesis: S_{1}[m + 1]

let X be finite set ; :: thesis: ( card X = m + 1 implies ex fp being FinSequence st

( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

assume A3: card X = m + 1 ; :: thesis: ex fp being FinSequence st

( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

then consider x being object such that

A4: x in X by CARD_1:27, XBOOLE_0:def 1;

set Y = X \ {x};

card (X \ {x}) = (card X) - (card {x}) by A4, EULER_1:4

.= (m + 1) - 1 by A3, CARD_1:30

.= m ;

then consider fp1 being FinSequence such that

A5: len fp1 = m and

A6: for a being Element of NAT st a in dom fp1 holds

fp1 . a in X \ {x} and

A7: fp1 is one-to-one by A2;

set fp = fp1 ^ <*x*>;

A8: len (fp1 ^ <*x*>) = m + 1 by A5, FINSEQ_2:16;

for a, b being object st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b holds

(fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

a = b ;

take fp1 ^ <*x*> ; :: thesis: ( len (fp1 ^ <*x*>) = m + 1 & ( for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds

(fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one )

for a being object st a in dom (fp1 ^ <*x*>) holds

(fp1 ^ <*x*>) . a in X

(fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one ) by A5, A21, FINSEQ_2:16; :: thesis: verum

end;assume A2: S

let X be finite set ; :: thesis: ( card X = m + 1 implies ex fp being FinSequence st

( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

assume A3: card X = m + 1 ; :: thesis: ex fp being FinSequence st

( len fp = m + 1 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

then consider x being object such that

A4: x in X by CARD_1:27, XBOOLE_0:def 1;

set Y = X \ {x};

card (X \ {x}) = (card X) - (card {x}) by A4, EULER_1:4

.= (m + 1) - 1 by A3, CARD_1:30

.= m ;

then consider fp1 being FinSequence such that

A5: len fp1 = m and

A6: for a being Element of NAT st a in dom fp1 holds

fp1 . a in X \ {x} and

A7: fp1 is one-to-one by A2;

set fp = fp1 ^ <*x*>;

A8: len (fp1 ^ <*x*>) = m + 1 by A5, FINSEQ_2:16;

for a, b being object st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b holds

(fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

proof

then A21:
for a, b being object st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & (fp1 ^ <*x*>) . a = (fp1 ^ <*x*>) . b holds
let a, b be object ; :: thesis: ( a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b implies (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b )

assume that

A9: a in dom (fp1 ^ <*x*>) and

A10: b in dom (fp1 ^ <*x*>) and

A11: a <> b ; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

A12: a in Seg (m + 1) by A8, A9, FINSEQ_1:def 3;

A13: b in Seg (m + 1) by A8, A10, FINSEQ_1:def 3;

reconsider a = a, b = b as Element of NAT by A9, A10;

end;assume that

A9: a in dom (fp1 ^ <*x*>) and

A10: b in dom (fp1 ^ <*x*>) and

A11: a <> b ; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

A12: a in Seg (m + 1) by A8, A9, FINSEQ_1:def 3;

A13: b in Seg (m + 1) by A8, A10, FINSEQ_1:def 3;

reconsider a = a, b = b as Element of NAT by A9, A10;

per cases
( a in Seg m or a = m + 1 )
by A12, FINSEQ_2:7;

end;

suppose A14:
a in Seg m
; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

end;

per cases
( b in Seg m or b = m + 1 )
by A13, FINSEQ_2:7;

end;

suppose
b in Seg m
; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

then A15:
b in dom fp1
by A5, FINSEQ_1:def 3;

then A16: (fp1 ^ <*x*>) . b = fp1 . b by FINSEQ_1:def 7;

A17: a in dom fp1 by A5, A14, FINSEQ_1:def 3;

then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def 7;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A7, A11, A17, A15, A16; :: thesis: verum

end;then A16: (fp1 ^ <*x*>) . b = fp1 . b by FINSEQ_1:def 7;

A17: a in dom fp1 by A5, A14, FINSEQ_1:def 3;

then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def 7;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A7, A11, A17, A15, A16; :: thesis: verum

suppose A18:
b = m + 1
; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

a in dom fp1
by A5, A14, FINSEQ_1:def 3;

then ( fp1 . a in X \ {x} & (fp1 ^ <*x*>) . a = fp1 . a ) by A6, FINSEQ_1:def 7;

then A19: not (fp1 ^ <*x*>) . a in {x} by XBOOLE_0:def 5;

(fp1 ^ <*x*>) . b = x by A5, A18, FINSEQ_1:42;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A19, TARSKI:def 1; :: thesis: verum

end;then ( fp1 . a in X \ {x} & (fp1 ^ <*x*>) . a = fp1 . a ) by A6, FINSEQ_1:def 7;

then A19: not (fp1 ^ <*x*>) . a in {x} by XBOOLE_0:def 5;

(fp1 ^ <*x*>) . b = x by A5, A18, FINSEQ_1:42;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A19, TARSKI:def 1; :: thesis: verum

suppose A20:
a = m + 1
; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

then
b in Seg m
by A11, A13, FINSEQ_2:7;

then b in dom fp1 by A5, FINSEQ_1:def 3;

then ( fp1 . b in X \ {x} & (fp1 ^ <*x*>) . b = fp1 . b ) by A6, FINSEQ_1:def 7;

then not (fp1 ^ <*x*>) . b in {x} by XBOOLE_0:def 5;

then (fp1 ^ <*x*>) . b <> x by TARSKI:def 1;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A5, A20, FINSEQ_1:42; :: thesis: verum

end;then b in dom fp1 by A5, FINSEQ_1:def 3;

then ( fp1 . b in X \ {x} & (fp1 ^ <*x*>) . b = fp1 . b ) by A6, FINSEQ_1:def 7;

then not (fp1 ^ <*x*>) . b in {x} by XBOOLE_0:def 5;

then (fp1 ^ <*x*>) . b <> x by TARSKI:def 1;

hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A5, A20, FINSEQ_1:42; :: thesis: verum

a = b ;

take fp1 ^ <*x*> ; :: thesis: ( len (fp1 ^ <*x*>) = m + 1 & ( for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds

(fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one )

for a being object st a in dom (fp1 ^ <*x*>) holds

(fp1 ^ <*x*>) . a in X

proof

hence
( len (fp1 ^ <*x*>) = m + 1 & ( for a being Element of NAT st a in dom (fp1 ^ <*x*>) holds
let a be object ; :: thesis: ( a in dom (fp1 ^ <*x*>) implies (fp1 ^ <*x*>) . a in X )

assume a in dom (fp1 ^ <*x*>) ; :: thesis: (fp1 ^ <*x*>) . a in X

then A22: a in Seg (m + 1) by A8, FINSEQ_1:def 3;

end;assume a in dom (fp1 ^ <*x*>) ; :: thesis: (fp1 ^ <*x*>) . a in X

then A22: a in Seg (m + 1) by A8, FINSEQ_1:def 3;

per cases
( a in Seg m or a = m + 1 )
by A22, FINSEQ_2:7;

end;

(fp1 ^ <*x*>) . a in X ) & fp1 ^ <*x*> is one-to-one ) by A5, A21, FINSEQ_2:16; :: thesis: verum

proof

for m being Nat holds S
set fp = <*> NAT;

let X be finite set ; :: thesis: ( card X = 0 implies ex fp being FinSequence st

( len fp = 0 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

assume card X = 0 ; :: thesis: ex fp being FinSequence st

( len fp = 0 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

take <*> NAT ; :: thesis: ( len (<*> NAT) = 0 & ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one )

thus len (<*> NAT) = 0 ; :: thesis: ( ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one )

thus ( ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one ) ; :: thesis: verum

end;let X be finite set ; :: thesis: ( card X = 0 implies ex fp being FinSequence st

( len fp = 0 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) )

assume card X = 0 ; :: thesis: ex fp being FinSequence st

( len fp = 0 & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one )

take <*> NAT ; :: thesis: ( len (<*> NAT) = 0 & ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one )

thus len (<*> NAT) = 0 ; :: thesis: ( ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one )

thus ( ( for a being Element of NAT st a in dom (<*> NAT) holds

(<*> NAT) . a in X ) & <*> NAT is one-to-one ) ; :: thesis: verum

hence ( card X = m implies ex fp being FinSequence st

( len fp = m & ( for a being Element of NAT st a in dom fp holds

fp . a in X ) & fp is one-to-one ) ) ; :: thesis: verum