let I be FinSequence-membered set ; :: thesis: for p being FinSequence holds card (p ^^ I) = card I
let p be FinSequence; :: thesis: card (p ^^ I) = card I
deffunc H₁( Element of I) -> set = p ^ $1;
consider f being Function such that
A1: ( dom f = I & ( for q being Element of I st q in I holds
f . q = H₁(q) ) ) from CLASSES1:sch 2();
A2: rng f = p ^^ I

proof

thus rng f c= p ^^ I :: according to XBOOLE_0:def 10 :: thesis: p ^^ I c= rng f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in p ^^ I )
reconsider x = a as set by TARSKI:1;
assume a in rng f ; :: thesis: a in p ^^ I
then consider b being object such that
A3: ( b in dom f & x = f . b ) by FUNCT_1:def 3;
reconsider b = b as Element of I by A1, A3;
a = H₁(b) by A1, A3;
hence a in p ^^ I by A1, A3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in p ^^ I or a in rng f )
reconsider x = a as set by TARSKI:1;
assume a in p ^^ I ; :: thesis: a in rng f
then consider q being Element of I such that
A4: ( a = p ^ q & q in I ) ;
x = f . q by A1, A4;
hence a in rng f by A1, A4, FUNCT_1:def 3; :: thesis: verum

end;

f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume A5: ( a in dom f & b in dom f ) ; :: thesis: ( not f . a = f . b or a = b )
then reconsider a = a, b = b as Element of I by A1;
( f . a = p ^ a & f . b = p ^ b ) by A1, A5;
hence ( not f . a = f . b or a = b ) by FINSEQ_1:33; :: thesis: verum

end;

hence card (p ^^ I) = card I by A1, A2, CARD_1:70; :: thesis: verum