let P be set ; :: thesis: for f being Function st rng f c= union P holds
ex p being Function st
( dom p = dom f & rng p c= P & f in product p )
let f be Function; :: thesis: ( rng f c= union P implies ex p being Function st
( dom p = dom f & rng p c= P & f in product p ) )
assume A1: rng f c= union P ; :: thesis: ex p being Function st
( dom p = dom f & rng p c= P & f in product p )
defpred S₁[ set , set ] means f . $1 in $2;
A2: for x being set st x in dom f holds
ex a being set st
( a in P & S₁[x,a] )

proof

let x be set ; :: thesis: ( x in dom f implies ex a being set st
( a in P & S₁[x,a] ) )
assume x in dom f ; :: thesis: ex a being set st
( a in P & S₁[x,a] )
then f . x in rng f by FUNCT_1:def 3;
then ex a being set st
( f . x in a & a in P ) by A1, TARSKI:def 4;
hence ex a being set st
( a in P & S₁[x,a] ) ; :: thesis: verum

end;

consider p being Function such that
A3: ( dom p = dom f & rng p c= P ) and
A4: for x being set st x in dom f holds
S₁[x,p . x] from FUNCT_1:sch 5(A2);
take p ; :: thesis: ( dom p = dom f & rng p c= P & f in product p )
thus ( dom p = dom f & rng p c= P & f in product p ) by A3, A4, CARD_3:def 5; :: thesis: verum