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₁[ object , object ] means ex D2 being set st
( D2 = $2 & f . $1 in D2 );
A2: for x being object st x in dom f holds
ex a being object st
( a in P & S₁[x,a] )

proof

let x be object ; :: thesis: ( x in dom f implies ex a being object st
( a in P & S₁[x,a] ) )
assume x in dom f ; :: thesis: ex a being object 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 object 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 object st x in dom f holds
S₁[x,p . x] from FUNCT_1:sch 6(A2);
take p ; :: thesis: ( dom p = dom f & rng p c= P & f in product p )
for x being object st x in dom f holds
f . x in p . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x in p . x )
assume x in dom f ; :: thesis: f . x in p . x
then S₁[x,p . x] by A4;
hence f . x in p . x ; :: thesis: verum

end;

hence ( dom p = dom f & rng p c= P & f in product p ) by A3, CARD_3:def 5; :: thesis: verum