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, Def2;
rng (g * f) c= rng g by RELAT_1:26;
then A4: rng (g * f) c= C by A3;
ex f9 being Function st
( f9 = f & dom f9 = A & rng f9 c= B ) by A1, Def2;
then dom (g * f) = A by A3, RELAT_1:27;
hence g * f in Funcs (A,C) by A4, Def2; :: thesis: verum