let x be object ; :: thesis: for f, g being Function st x in dom f holds
(g * f) . x = g . (f . x)
let f, g be Function; :: thesis: ( x in dom f implies (g * f) . x = g . (f . x) )
assume A1: x in dom f ; :: thesis: (g * f) . x = g . (f . x)

per cases ( f . x in dom g or not f . x in dom g ) ;

suppose f . x in dom g ; :: thesis: (g * f) . x = g . (f . x)

then x in dom (g * f) by A1, Th11;
hence (g * f) . x = g . (f . x) by Th12; :: thesis: verum

end;

suppose A2: not f . x in dom g ; :: thesis: (g * f) . x = g . (f . x)

then not x in dom (g * f) by Th11;
hence (g * f) . x = {} by Def2
.= g . (f . x) by A2, Def2 ;
:: thesis: verum

end;

end;