let f, g be Function; :: thesis: ( rng f c= rng g implies ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h ) )
assume A1: rng f c= rng g ; :: thesis: ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h )
defpred S₁[ set , set ] means f . $1 = g . $2;
A2: for x being set st x in dom f holds
ex y being set st
( y in dom g & S₁[x,y] ) by A1, GRAPH_5:2;
consider h being Function of (dom f),(dom g) such that
A3: for x being set st x in dom f holds
S₁[x,h . x] from FUNCT_2:sch 1(A2);

per cases ( dom g = {} or dom g <> {} ) ;

suppose dom g = {} ; :: thesis: ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h )

then rng g = {} by RELAT_1:65;
then rng f = {} by A1;
then ( f = g * {} & dom {} = dom f & rng {} c= dom g ) by RELAT_1:64, XBOOLE_1:2;
hence ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h ) ; :: thesis: verum

end;

suppose dom g <> {} ; :: thesis: ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h )

then A4: ( dom h = dom f & rng h c= dom g ) by FUNCT_2:def 1, RELAT_1:def 19;
then A5: dom (g * h) = dom f by RELAT_1:46;

now

let x be set ; :: thesis: ( x in dom f implies f . x = (g * h) . x )
assume A6: x in dom f ; :: thesis: f . x = (g * h) . x
thus f . x = g . (h . x) by A3, A6
.= (g * h) . x by A5, A6, FUNCT_1:22 ; :: thesis: verum

end;

then f = g * h by A5, FUNCT_1:9;
hence ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h ) by A4; :: thesis: verum

end;

end;