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 S1[ object , object ] means f . $1 = g . $2;
A2: for x being object st x in dom f holds
ex y being object st
( y in dom g & S1[x,y] ) by A1, FUNCT_1:114;
consider h being Function of (dom f),(dom g) such that
A3: for x being object st x in dom f holds
S1[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:42;
then A4: f = g * {} by A1;
rng {} c= dom g ;
hence ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h ) by A4; :: thesis: verum
end;
suppose A5: dom g <> {} ; :: thesis: ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h )
A6: rng h c= dom g by RELAT_1:def 19;
A7: dom h = dom f by A5, FUNCT_2:def 1;
then A8: dom (g * h) = dom f by A6, RELAT_1:27;
now :: thesis: for x being object st x in dom f holds
f . x = (g * h) . x
let x be object ; :: thesis: ( x in dom f implies f . x = (g * h) . x )
assume A9: x in dom f ; :: thesis: f . x = (g * h) . x
thus f . x = g . (h . x) by A3, A9
.= (g * h) . x by A8, A9, FUNCT_1:12 ; :: thesis: verum
end;
hence ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h ) by A7, A6, A8, FUNCT_1:2; :: thesis: verum
end;
end;