let x be object ; :: thesis: for f, g being Function st x in dom (g * f) holds
(g * f) . x = g . (f . x)
let f, g 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 object such that
A2: [x,y] in g * f by XTUPLE_0:def 12;
consider z being object such that
A3: [x,z] in f and
A4: [z,y] in g by A2, RELAT_1:def 8;
reconsider z = z, y = y as set by TARSKI:1;
x in dom f by A3, XTUPLE_0:def 12;
then A5: z = f . x by A3, Def2;
then f . x in dom g by A4, XTUPLE_0:def 12;
then y = g . (f . x) by A4, A5, Def2;
hence (g * f) . x = g . (f . x) by A1, A2, Def2; :: thesis: verum