let X, Y, Z be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)
let g be Function of Y,Z; :: thesis: (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

proof

let x be Point of X0; :: thesis: G . x = (g * F0) . x
the carrier of X0 c= the carrier of X by BORSUK_1:1;
then reconsider y = x as Element of X by TARSKI:def 3;
thus G . x = (g * f) . y by FUNCT_1:49
.= g . (f . y) by FUNCT_2:15
.= g . (F0 . x) by FUNCT_1:49
.= (g * F0) . x by FUNCT_2:15 ; :: thesis: verum

end;

hence (g * f) | X0 = g * (f | X0) by FUNCT_2:63; :: thesis: verum