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 )
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 ) )
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 );
A1: S₁[ 0 ]

proof

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 )
set fp = <*> NAT ;
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;

A2: 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 A3: 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 A4: 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
A5: x in X by CARD_1:47, XBOOLE_0:def 1;
set Y = X \ {x};
card (X \ {x}) = (card X) - (card {x}) by A5, EULER_1:5
.= (m + 1) - 1 by A4, CARD_1:50
.= m ;
then consider fp1 being FinSequence such that
A6: ( len fp1 = m & ( for a being Element of NAT st a in dom fp1 holds
fp1 . a in X \ {x} ) & fp1 is one-to-one ) by A3;
set fp = fp1 ^ <*x*>;
A7: len (fp1 ^ <*x*>) = m + 1 by A6, FINSEQ_2:19;
A8: 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 A9: a in Seg (m + 1) by A7, FINSEQ_1:def 3;

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

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

then A10: a in dom fp1 by A6, FINSEQ_1:def 3;
then (fp1 ^ <*x*>) . a = fp1 . a by FINSEQ_1:def 7;
then (fp1 ^ <*x*>) . a in X \ {x} by A6, A10;
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 A5, A6, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

A11: 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 A12: ( a in dom (fp1 ^ <*x*>) & b in dom (fp1 ^ <*x*>) & a <> b ) ; :: thesis: (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b
then A13: ( a in Seg (m + 1) & b in Seg (m + 1) & a <> b ) by A7, FINSEQ_1:def 3;
reconsider a = a, b = b as Element of NAT by A12;

per cases ( a in Seg m or a = m + 1 ) by A13, 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: ( a in dom fp1 & b in dom fp1 ) by A6, A14, FINSEQ_1:def 3;
then ( (fp1 ^ <*x*>) . a = fp1 . a & (fp1 ^ <*x*>) . b = fp1 . b ) by FINSEQ_1:def 7;
hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A6, A12, A15, FUNCT_1:def 8; :: thesis: verum

end;

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

then A16: (fp1 ^ <*x*>) . b = x by A6, FINSEQ_1:59;
a in dom fp1 by A6, A14, FINSEQ_1:def 3;
then ( fp1 . a in X \ {x} & (fp1 ^ <*x*>) . a = fp1 . a ) by A6, FINSEQ_1:def 7;
then not (fp1 ^ <*x*>) . a in {x} by XBOOLE_0:def 5;
hence (fp1 ^ <*x*>) . a <> (fp1 ^ <*x*>) . b by A16, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

then b in Seg m by A13, FINSEQ_2:8;
then b in dom fp1 by A6, 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 A6, A17, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

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 )
fp1 ^ <*x*> is one-to-one

proof

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 by A11;
hence fp1 ^ <*x*> is one-to-one by FUNCT_1:def 8; :: thesis: verum

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 A6, A8, FINSEQ_2:19; :: thesis: verum

end;

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