let A be set ; :: thesis: ( A is finite implies ex p being FinSequence st
( rng p = A & p is one-to-one ) )
defpred S1[ set ] means ex p being FinSequence st
( rng p = $1 & p is one-to-one );
rng {} = {} ;
then A1: S1[ {} ] ;
now :: thesis: for B, C being set st B in A & C c= A & ex p being FinSequence st
( rng p = C & p is one-to-one ) holds
ex p being FinSequence st
( rng p = C \/ {B} & p is one-to-one )
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 :: thesis: ( not B in C implies ex q being set st
( rng q = C \/ {B} & q is one-to-one ) )
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:31
.= C \/ {B} by A2, FINSEQ_1:38 ; :: thesis: q is one-to-one
thus q is one-to-one :: thesis: verum
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom q or not y in dom 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 :: thesis: ( k in dom p & ex n being Nat st
( n in dom <*B*> & l = (len p) + n ) implies x = y )
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:2, FINSEQ_1:38;
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 3; :: thesis: verum
end;
A13: now :: thesis: ( l in dom p & ex n being Nat st
( n in dom <*B*> & k = (len p) + n ) implies x = y )
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:2, FINSEQ_1:38;
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 3; :: thesis: verum
end;
A18: now :: thesis: ( ex m1 being Nat st
( m1 in dom <*B*> & k = (len p) + m1 ) & ex m2 being Nat st
( m2 in dom <*B*> & l = (len p) + m2 ) implies x = y )
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:2, 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:2, FINSEQ_1:def 8;
hence x = y by A20, A23, A21, TARSKI:def 1; :: thesis: verum
end;
now :: thesis: ( k in dom p & l in dom p implies x = y )
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; :: thesis: verum
end;
hence x = y by A6, A8, A13, A18, FINSEQ_1:25; :: thesis: verum
end;
end;
now :: thesis: ( B in C implies ex q being FinSequence st
( rng q = C \/ {B} & q is one-to-one ) )
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:40; :: 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 & S1[C] holds
S1[C \/ {B}] ;
assume A27: A is finite ; :: thesis: ex p being FinSequence st
( rng p = A & p is one-to-one )
thus S1[A] from FINSET_1:sch 2(A27, A1, A26); :: thesis: verum