let A, B, C be set ; :: thesis: for f, g being Function st f in Funcs A,B & g in Funcs B,C holds
g * f in Funcs A,C
let f, g be Function; :: thesis: ( f in Funcs A,B & g in Funcs B,C implies g * f in Funcs A,C )
assume that
A1: f in Funcs A,B and
A2: g in Funcs B,C ; :: thesis: g * f in Funcs A,C
A3: ex g9 being Function st
( g9 = g & dom g9 = B & rng g9 c= C ) by A2, FUNCT_2:def 2;
rng (g * f) c= rng g by RELAT_1:45;
then A4: rng (g * f) c= C by A3, XBOOLE_1:1;
ex f9 being Function st
( f9 = f & dom f9 = A & rng f9 c= B ) by A1, FUNCT_2:def 2;
then dom (g * f) = A by A3, RELAT_1:46;
hence g * f in Funcs A,C by A4, FUNCT_2:def 2; :: thesis: verum