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

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

hence
(g * f) | X0 = g * (f | X0)
by FUNCT_2:63; :: thesis: verum
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;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