let X, Y, Z be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of Y,Z holds free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)
let f be Function of X,Y; :: thesis: for g being Function of Y,Z holds free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)
let g be Function of Y,Z; :: thesis: free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)
set f2 = (free_magmaF g) * (free_magmaF f);
reconsider f9 = (canon_image (Z,1)) * (g * f) as Function of X,(free_magma Z) by Th38;
for a, b being Element of (free_magma X) holds ((free_magmaF g) * (free_magmaF f)) . (a * b) = (((free_magmaF g) * (free_magmaF f)) . a) * (((free_magmaF g) * (free_magmaF f)) . b)

proof

let a, b be Element of (free_magma X); :: thesis: ((free_magmaF g) * (free_magmaF f)) . (a * b) = (((free_magmaF g) * (free_magmaF f)) . a) * (((free_magmaF g) * (free_magmaF f)) . b)
a * b in the carrier of (free_magma X) ;
then A1: a * b in dom ((free_magmaF g) * (free_magmaF f)) by FUNCT_2:def 1;
( a in the carrier of (free_magma X) & b in the carrier of (free_magma X) ) ;
then A2: ( a in dom (free_magmaF f) & b in dom (free_magmaF f) ) by FUNCT_2:def 1;
thus ((free_magmaF g) * (free_magmaF f)) . (a * b) = (free_magmaF g) . ((free_magmaF f) . (a * b)) by A1, FUNCT_1:12
.= (free_magmaF g) . (((free_magmaF f) . a) * ((free_magmaF f) . b)) by GROUP_6:def 6
.= ((free_magmaF g) . ((free_magmaF f) . a)) * ((free_magmaF g) . ((free_magmaF f) . b)) by GROUP_6:def 6
.= (((free_magmaF g) * (free_magmaF f)) . a) * ((free_magmaF g) . ((free_magmaF f) . b)) by A2, FUNCT_1:13
.= (((free_magmaF g) * (free_magmaF f)) . a) * (((free_magmaF g) * (free_magmaF f)) . b) by A2, FUNCT_1:13 ; :: thesis: verum

end;

then A3: (free_magmaF g) * (free_magmaF f) is multiplicative by GROUP_6:def 6;
A4: dom (f9 * ((canon_image (X,1)) ")) c= dom ((canon_image (X,1)) ") by RELAT_1:25;
rng (canon_image (X,1)) c= the carrier of (free_magma X) ;
then dom ((canon_image (X,1)) ") c= the carrier of (free_magma X) by FUNCT_1:33;
then dom (f9 * ((canon_image (X,1)) ")) c= the carrier of (free_magma X) by A4;
then A5: dom (f9 * ((canon_image (X,1)) ")) c= dom ((free_magmaF g) * (free_magmaF f)) by FUNCT_2:def 1;
for x being object st x in dom (f9 * ((canon_image (X,1)) ")) holds
((free_magmaF g) * (free_magmaF f)) . x = (f9 * ((canon_image (X,1)) ")) . x

proof

let x be object ; :: thesis: ( x in dom (f9 * ((canon_image (X,1)) ")) implies ((free_magmaF g) * (free_magmaF f)) . x = (f9 * ((canon_image (X,1)) ")) . x )
assume A6: x in dom (f9 * ((canon_image (X,1)) ")) ; :: thesis: ((free_magmaF g) * (free_magmaF f)) . x = (f9 * ((canon_image (X,1)) ")) . x
free_magmaF f extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") by Def21;
then A7: ( dom (((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")) c= dom (free_magmaF f) & ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") tolerates free_magmaF f ) ;
A8: x in dom ((canon_image (X,1)) ") by A6, FUNCT_1:11;
X c= dom f by FUNCT_2:def 1;
then dom (canon_image (X,1)) c= dom f by Lm3;
then rng ((canon_image (X,1)) ") c= dom f by FUNCT_1:33;
then A9: x in dom (f * ((canon_image (X,1)) ")) by A8, RELAT_1:27;
rng (f * ((canon_image (X,1)) ")) c= Y ;
then rng (f * ((canon_image (X,1)) ")) c= dom (canon_image (Y,1)) by Lm3;
then x in dom ((canon_image (Y,1)) * (f * ((canon_image (X,1)) "))) by A9, RELAT_1:27;
then A10: x in dom (((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")) by RELAT_1:36;
set y = (f * ((canon_image (X,1)) ")) . x;
free_magmaF g extends ((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ") by Def21;
then A11: ( dom (((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ")) c= dom (free_magmaF g) & ((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ") tolerates free_magmaF g ) ;
(f * ((canon_image (X,1)) ")) . x in rng (f * ((canon_image (X,1)) ")) by A9, FUNCT_1:3;
then A12: (f * ((canon_image (X,1)) ")) . x in Y ;
then A13: (f * ((canon_image (X,1)) ")) . x in dom (canon_image (Y,1)) by Lm3;
then A14: (canon_image (Y,1)) . ((f * ((canon_image (X,1)) ")) . x) in rng (canon_image (Y,1)) by FUNCT_1:3;
Y c= dom g by FUNCT_2:def 1;
then A15: dom (canon_image (Y,1)) c= dom g by Lm3;
rng g c= Z ;
then rng g c= dom (canon_image (Z,1)) by Lm3;
then dom (canon_image (Y,1)) c= dom ((canon_image (Z,1)) * g) by A15, RELAT_1:27;
then A16: rng ((canon_image (Y,1)) ") c= dom ((canon_image (Z,1)) * g) by FUNCT_1:33;
rng (canon_image (Y,1)) c= dom ((canon_image (Y,1)) ") by FUNCT_1:33;
then A17: rng (canon_image (Y,1)) c= dom (((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ")) by A16, RELAT_1:27;
A18: rng (canon_image (Y,1)) c= dom ((canon_image (Y,1)) ") by FUNCT_1:33;
dom (canon_image (Y,1)) = Y by Lm3;
then A19: (f * ((canon_image (X,1)) ")) . x in dom (((canon_image (Y,1)) ") * (canon_image (Y,1))) by A12, A18, RELAT_1:27;
A20: ((canon_image (Z,1)) * g) * (f * ((canon_image (X,1)) ")) = (canon_image (Z,1)) * (g * (f * ((canon_image (X,1)) "))) by RELAT_1:36
.= (canon_image (Z,1)) * ((g * f) * ((canon_image (X,1)) ")) by RELAT_1:36
.= ((canon_image (Z,1)) * (g * f)) * ((canon_image (X,1)) ") by RELAT_1:36 ;
thus ((free_magmaF g) * (free_magmaF f)) . x = (free_magmaF g) . ((free_magmaF f) . x) by A6, A5, FUNCT_1:12
.= (free_magmaF g) . ((((canon_image (Y,1)) * f) * ((canon_image (X,1)) ")) . x) by A10, A7, PARTFUN1:53
.= (free_magmaF g) . (((canon_image (Y,1)) * (f * ((canon_image (X,1)) "))) . x) by RELAT_1:36
.= (free_magmaF g) . ((canon_image (Y,1)) . ((f * ((canon_image (X,1)) ")) . x)) by A9, FUNCT_1:13
.= (((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ")) . ((canon_image (Y,1)) . ((f * ((canon_image (X,1)) ")) . x)) by A17, A14, A11, PARTFUN1:53
.= ((((canon_image (Z,1)) * g) * ((canon_image (Y,1)) ")) * (canon_image (Y,1))) . ((f * ((canon_image (X,1)) ")) . x) by A13, FUNCT_1:13
.= (((canon_image (Z,1)) * g) * (((canon_image (Y,1)) ") * (canon_image (Y,1)))) . ((f * ((canon_image (X,1)) ")) . x) by RELAT_1:36
.= ((canon_image (Z,1)) * g) . ((((canon_image (Y,1)) ") * (canon_image (Y,1))) . ((f * ((canon_image (X,1)) ")) . x)) by A19, FUNCT_1:13
.= ((canon_image (Z,1)) * g) . ((f * ((canon_image (X,1)) ")) . x) by A13, FUNCT_1:34
.= (f9 * ((canon_image (X,1)) ")) . x by A20, A9, FUNCT_1:13 ; :: thesis: verum

end;

then (free_magmaF g) * (free_magmaF f) tolerates f9 * ((canon_image (X,1)) ") by A5, PARTFUN1:53;
then (free_magmaF g) * (free_magmaF f) extends f9 * ((canon_image (X,1)) ") by A5;
hence free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f) by Def21, A3; :: thesis: verum