let X, Y be set ; :: thesis: ( X is_finer_than Y implies for p being FinSequence of X ex q being FinSequence of Y st product p c= product q )
assume A1: for a being set st a in X holds
ex b being set st
( b in Y & a c= b ) ; :: according to SETFAM_1:def 2 :: thesis: for p being FinSequence of X ex q being FinSequence of Y st product p c= product q
let p be FinSequence of X; :: thesis: ex q being FinSequence of Y st product p c= product q
defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & p . $1 c= D2 );
A2: for i being object st i in dom p holds
ex y being object st
( y in Y & S₁[i,y] )

proof

let i be object ; :: thesis: ( i in dom p implies ex y being object st
( y in Y & S₁[i,y] ) )
assume A3: i in dom p ; :: thesis: ex y being object st
( y in Y & S₁[i,y] )
reconsider i = i as set by TARSKI:1;
p . i in rng p by FUNCT_1:def 3, A3;
then p . i in X ;
then consider b being set such that
A4: ( b in Y & p . i c= b ) by A1;
take b ; :: thesis: ( b in Y & S₁[i,b] )
thus ( b in Y & S₁[i,b] ) by A4; :: thesis: verum

end;

consider q being Function such that
A5: ( dom q = dom p & rng q c= Y & ( for i being object st i in dom p holds
S₁[i,q . i] ) ) from FUNCT_1:sch 6(A2);
dom p = Seg (len p) by FINSEQ_1:def 3;
then q is FinSequence by A5, FINSEQ_1:def 2;
then A6: q is FinSequence of Y by A5, FINSEQ_1:def 4;
for i being object st i in dom p holds
p . i c= q . i

proof

let i be object ; :: thesis: ( i in dom p implies p . i c= q . i )
assume i in dom p ; :: thesis: p . i c= q . i
then S₁[i,q . i] by A5;
hence p . i c= q . i ; :: thesis: verum

end;

then product p c= product q by A5, CARD_3:27;
hence ex q being FinSequence of Y st product p c= product q by A6; :: thesis: verum