let A be set ; :: thesis: ( A is finite implies ex p being FinSequence st
( rng p = A & p is one-to-one ) )
defpred S₁[ set ] means ex p being FinSequence st
( rng p = $1 & p is one-to-one );
rng {} = {} ;
then A1: S₁[ {} ] ;

now

let B, C be set ; :: thesis: ( B in A & C c= A & ex p being FinSequence st
( rng p = C & p is one-to-one ) implies ex p being FinSequence st
( rng p = C \/ {B} & p is one-to-one ) )
assume that
B in A and
C c= A ; :: thesis: ( ex p being FinSequence st
( rng p = C & p is one-to-one ) implies ex p being FinSequence st
( rng p = C \/ {B} & p is one-to-one ) )
given p being FinSequence such that A2: rng p = C and
A3: p is one-to-one ; :: thesis: ex p being FinSequence st
( rng p = C \/ {B} & p is one-to-one )

A4: now

assume A5: not B in C ; :: thesis: ex q being set st
( rng q = C \/ {B} & q is one-to-one )
take q = p ^ <*B*>; :: thesis: ( rng q = C \/ {B} & q is one-to-one )
thus rng q = (rng p) \/ (rng <*B*>) by FINSEQ_1:44
.= C \/ {B} by A2, FINSEQ_1:55 ; :: thesis: q is one-to-one
thus q is one-to-one :: thesis: verum

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 q or not b₁ in proj1 q or not q . x = q . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 q or not y in proj1 q or not q . x = q . y or x = y )
assume that
A6: ( x in dom q & y in dom q ) and
A7: q . x = q . y ; :: thesis: x = y
reconsider k = x, l = y as Element of NAT by A6;

A8: now

assume A9: k in dom p ; :: thesis: ( ex n being Nat st
( n in dom <*B*> & l = (len p) + n ) implies x = y )
given n being Nat such that A10: n in dom <*B*> and
A11: l = (len p) + n ; :: thesis: x = y
n in {1} by A10, FINSEQ_1:4, FINSEQ_1:55;
then A12: n = 1 by TARSKI:def 1;
<*B*> . n = q . k by A7, A10, A11, FINSEQ_1:def 7
.= p . k by A9, FINSEQ_1:def 7 ;
then B = p . k by A12, FINSEQ_1:def 8;
hence x = y by A2, A5, A9, FUNCT_1:def 5; :: thesis: verum

end;

A13: now

assume A14: l in dom p ; :: thesis: ( ex n being Nat st
( n in dom <*B*> & k = (len p) + n ) implies x = y )
given n being Nat such that A15: n in dom <*B*> and
A16: k = (len p) + n ; :: thesis: x = y
n in {1} by A15, FINSEQ_1:4, FINSEQ_1:55;
then A17: n = 1 by TARSKI:def 1;
<*B*> . n = q . l by A7, A15, A16, FINSEQ_1:def 7
.= p . l by A14, FINSEQ_1:def 7 ;
then B = p . l by A17, FINSEQ_1:def 8;
hence x = y by A2, A5, A14, FUNCT_1:def 5; :: thesis: verum

end;

A18: now

given m1 being Nat such that A19: m1 in dom <*B*> and
A20: k = (len p) + m1 ; :: thesis: ( ex m2 being Nat st
( m2 in dom <*B*> & l = (len p) + m2 ) implies x = y )
m1 in {1} by A19, FINSEQ_1:4, FINSEQ_1:def 8;
then A21: m1 = 1 by TARSKI:def 1;
given m2 being Nat such that A22: m2 in dom <*B*> and
A23: l = (len p) + m2 ; :: thesis: x = y
m2 in {1} by A22, FINSEQ_1:4, FINSEQ_1:def 8;
hence x = y by A20, A23, A21, TARSKI:def 1; :: thesis: verum

end;

now

assume A24: ( k in dom p & l in dom p ) ; :: thesis: x = y
then ( q . k = p . k & q . l = p . l ) by FINSEQ_1:def 7;
hence x = y by A3, A7, A24, FUNCT_1:def 8; :: thesis: verum

end;

hence x = y by A6, A8, A13, A18, FINSEQ_1:38; :: thesis: verum

end;

end;

now

assume A25: B in C ; :: thesis: ex q being FinSequence st
( rng q = C \/ {B} & q is one-to-one )
take q = p; :: thesis: ( rng q = C \/ {B} & q is one-to-one )
thus ( rng q = C \/ {B} & q is one-to-one ) by A2, A3, A25, ZFMISC_1:46; :: thesis: verum

end;

hence ex p being FinSequence st
( rng p = C \/ {B} & p is one-to-one ) by A4; :: thesis: verum

end;

then A26: for B, C being set st B in A & C c= A & S₁[C] holds
S₁[C \/ {B}] ;
assume A27: A is finite ; :: thesis: ex p being FinSequence st
( rng p = A & p is one-to-one )
thus S₁[A] from FINSET_1:sch 2(A27, A1, A26); :: thesis: verum