let x be set ; :: thesis: for g, f being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)
let g, f be Function; :: thesis: ( x in dom (g * f) implies (g * f) . x = g . (f . x) )
set h = g * f;
assume A1: x in dom (g * f) ; :: thesis: (g * f) . x = g . (f . x)
then consider y being set such that
A2: [x,y] in g * f by RELAT_1:def 4;
consider z being set such that
A3: [x,z] in f and
A4: [z,y] in g by A2, RELAT_1:def 8;
x in dom f by A3, RELAT_1:def 4;
then A5: z = f . x by A3, Def4;
then f . x in dom g by A4, RELAT_1:def 4;
then y = g . (f . x) by A4, A5, Def4;
hence (g * f) . x = g . (f . x) by A1, A2, Def4; :: thesis: verum