let X, Y, Z be non empty TopSpace; for X0 being non empty SubSpace of X
for f being Function of X,Y
for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)
let X0 be non empty SubSpace of X; for f being Function of X,Y
for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)
let f be Function of X,Y; for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)
let g be Function of Y,Z; (g * f) | X0 = g * (f | X0)
set h = g * f;
(g * f) | X0 = (g * f) | the carrier of X0
;
then reconsider G = (g * f) | the carrier of X0 as Function of X0,Z ;
f | X0 = f | the carrier of X0
;
then reconsider F0 = f | the carrier of X0 as Function of X0,Y ;
set F = g * F0;
for x being Point of X0 holds G . x = (g * F0) . x
hence
(g * f) | X0 = g * (f | X0)
by FUNCT_2:63; verum