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₁[ 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 Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: S₁[m] ; :: thesis: S₁[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 set such that
A4: x in X by CARD_1:47, XBOOLE_0:def 1;
set Y = X \ {x};
card (X \ {x}) = (card X) - (card {x}) by A4, EULER_1:5
.= (m + 1) - 1 by A3, CARD_1:50
.= 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:19;
for a, b being set st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b holds
(fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b

proof

let a, b be set ; :: 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;

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

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

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

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, FUNCT_1:def 8; :: thesis: verum

end;

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:59;
hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A19, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

then b in Seg m by A11, A13, FINSEQ_2:8;
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:59; :: thesis: verum

end;

end;

end;

then A21: for a, b being set st a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & (fp1 ^ <*x*>) . a = (fp1 ^ <*x*>) . b holds
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 Element of NAT st a in dom (fp1 ^ <*x*>) holds
(fp1 ^ <*x*>) . a in X

proof

let a be Element of NAT ; :: 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;

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

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

then A23: a in dom fp1 by A5, FINSEQ_1:def 3;
then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def 7;
then (fp1 ^ <*x*>) . a in X \ {x} by A6, A23;
hence (fp1 ^ <*x*>) . a in X ; :: thesis: verum

end;

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

hence (fp1 ^ <*x*>) . a in X by A4, A5, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence ( 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 ) by A5, A21, FINSEQ_2:19, FUNCT_1:def 8; :: thesis: verum

end;

A24: S₁[ 0 ]

proof

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;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(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