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₁[ set , set ] means p . $1 c= $2;
A2: for i being set st i in dom p holds
ex y being set st
( y in Y & S₁[i,y] )

proof

let i be set ; :: thesis: ( i in dom p implies ex y being set st
( y in Y & S₁[i,y] ) )
assume i in dom p ; :: thesis: ex y being set st
( y in Y & S₁[i,y] )
then ( p . i in rng p & rng p c= X ) by FUNCT_1:def 5;
hence ex y being set st
( y in Y & S₁[i,y] ) by A1; :: thesis: verum

end;

consider q being Function such that
A3: ( dom q = dom p & rng q c= Y & ( for i being set st i in dom p holds
S₁[i,q . i] ) ) from WELLORD2:sch 1(A2);
dom p = Seg (len p) by FINSEQ_1:def 3;
then q is FinSequence by A3, FINSEQ_1:def 2;
then ( q is FinSequence of Y & product p c= product q ) by A3, CARD_3:38, FINSEQ_1:def 4;
hence ex q being FinSequence of Y st product p c= product q ; :: thesis: verum