let F1 be finite set ; :: thesis: for E1 being Enumeration of F1
for p being Function st union F1 c= dom p & p | (union F1) is one-to-one holds
( (.: p) * E1 is Enumeration of (.: p) .: F1 & card E1 = card ((.: p) * E1) )
let E1 be Enumeration of F1; :: thesis: for p being Function st union F1 c= dom p & p | (union F1) is one-to-one holds
( (.: p) * E1 is Enumeration of (.: p) .: F1 & card E1 = card ((.: p) * E1) )
let f be Function; :: thesis: ( union F1 c= dom f & f | (union F1) is one-to-one implies ( (.: f) * E1 is Enumeration of (.: f) .: F1 & card E1 = card ((.: f) * E1) ) )
assume A1: ( union F1 c= dom f & f | (union F1) is one-to-one ) ; :: thesis: ( (.: f) * E1 is Enumeration of (.: f) .: F1 & card E1 = card ((.: f) * E1) )
set fu = f | (union F1);
set If = .: f;
A2: rng E1 = F1 by RLAFFIN3:def 1;
( F1 c= bool (union F1) & bool (union F1) c= bool (dom f) ) by A1, ZFMISC_1:67, ZFMISC_1:82;
then F1 c= bool (dom f) ;
then F1 c= dom (.: f) by FUNCT_3:def 1;
then A3: ( dom ((.: f) * E1) = dom E1 & dom E1 = Seg (len E1) ) by A2, RELAT_1:27, FINSEQ_1:def 3;
then reconsider fE1 = (.: f) * E1 as FinSequence by FINSEQ_1:def 2;
A4: dom (f | (union F1)) = union F1 by A1, RELAT_1:62;
A5: fE1 is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom fE1 or not x2 in dom fE1 or not fE1 . x1 = fE1 . x2 or x1 = x2 )
assume A6: ( x1 in dom fE1 & x2 in dom fE1 & fE1 . x1 = fE1 . x2 ) ; :: thesis: x1 = x2
A7: ( x1 in dom E1 & E1 . x1 in dom (.: f) & fE1 . x1 = (.: f) . (E1 . x1) ) by A6, FUNCT_1:11, FUNCT_1:12;
then A8: ( fE1 . x1 = f .: (E1 . x1) & E1 . x1 in F1 ) by A2, FUNCT_3:7, FUNCT_1:def 3;
then A9: fE1 . x1 = (f | (union F1)) .: (E1 . x1) by RELAT_1:129, ZFMISC_1:74;
A10: ( x2 in dom E1 & E1 . x2 in dom (.: f) & fE1 . x2 = (.: f) . (E1 . x2) ) by A6, FUNCT_1:11, FUNCT_1:12;
then ( fE1 . x2 = f .: (E1 . x2) & E1 . x2 in F1 ) by A2, FUNCT_3:7, FUNCT_1:def 3;
then ( E1 . x2 = ((f | (union F1)) ") .: ((f | (union F1)) .: (E1 . x2)) & ((f | (union F1)) ") .: ((f | (union F1)) .: (E1 . x2)) = ((f | (union F1)) ") .: ((f | (union F1)) .: (E1 . x1)) & ((f | (union F1)) ") .: ((f | (union F1)) .: (E1 . x1)) = E1 . x1 ) by A1, FUNCT_1:107, A4, A6, A8, A9, RELAT_1:129, ZFMISC_1:74;
hence x1 = x2 by A7, A10, FUNCT_1:def 4; :: thesis: verum

end;

A11: rng fE1 c= (.: f) .: F1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fE1 or y in (.: f) .: F1 )
assume y in rng fE1 ; :: thesis: y in (.: f) .: F1
then consider x being object such that
A12: ( x in dom fE1 & fE1 . x = y ) by FUNCT_1:def 3;
A13: ( x in dom E1 & E1 . x in dom (.: f) & fE1 . x = (.: f) . (E1 . x) ) by A12, FUNCT_1:11, FUNCT_1:12;
then ( fE1 . x = f .: (E1 . x) & E1 . x in F1 ) by A2, FUNCT_3:7, FUNCT_1:def 3;
hence y in (.: f) .: F1 by A13, A12, FUNCT_1:def 6; :: thesis: verum

end;

(.: f) .: F1 c= rng fE1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (.: f) .: F1 or y in rng fE1 )
assume y in (.: f) .: F1 ; :: thesis: y in rng fE1
then consider x being object such that
A14: ( x in dom (.: f) & x in F1 & y = (.: f) . x ) by FUNCT_1:def 6;
consider z being object such that
A15: ( z in dom E1 & E1 . z = x ) by A2, A14, FUNCT_1:def 3;
( fE1 . z = y & z in dom fE1 ) by A15, A14, FUNCT_1:11, FUNCT_1:13;
hence y in rng fE1 by FUNCT_1:def 3; :: thesis: verum

end;

then rng fE1 = (.: f) .: F1 by A11;
hence ( (.: f) * E1 is Enumeration of (.: f) .: F1 & card E1 = card ((.: f) * E1) ) by A5, RLAFFIN3:def 1, A3, FINSEQ_3:29; :: thesis: verum