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 f1 = free_magmaF (g * 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 Th39;
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 A2: 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 A3: ( 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 A2, FUNCT_1:22
.= (free_magmaF g) . (((free_magmaF f) . a) * ((free_magmaF f) . b)) by GROUP_6:def 7
.= ((free_magmaF g) . ((free_magmaF f) . a)) * ((free_magmaF g) . ((free_magmaF f) . b)) by GROUP_6:def 7
.= (((free_magmaF g) * (free_magmaF f)) . a) * ((free_magmaF g) . ((free_magmaF f) . b)) by A3, FUNCT_1:23
.= (((free_magmaF g) * (free_magmaF f)) . a) * (((free_magmaF g) * (free_magmaF f)) . b) by A3, FUNCT_1:23 ; :: thesis: verum

end;

then A4: (free_magmaF g) * (free_magmaF f) is multiplicative by GROUP_6:def 7;
A5: dom (f9 * ((canon_image X,1) " )) c= dom ((canon_image X,1) " ) by RELAT_1:44;
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:55;
then dom (f9 * ((canon_image X,1) " )) c= the carrier of (free_magma X) by A5, XBOOLE_1:1;
then A6: dom (f9 * ((canon_image X,1) " )) c= dom ((free_magmaF g) * (free_magmaF f)) by FUNCT_2:def 1;
for x being set 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 set ; :: thesis: ( x in dom (f9 * ((canon_image X,1) " )) implies ((free_magmaF g) * (free_magmaF f)) . x = (f9 * ((canon_image X,1) " )) . x )
assume A7: 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 Def22;
then A8: ( 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 ) by Def3;
A9: x in dom ((canon_image X,1) " ) by A7, FUNCT_1:21;
X c= dom f by FUNCT_2:def 1;
then dom (canon_image X,1) c= dom f by Lm2;
then rng ((canon_image X,1) " ) c= dom f by FUNCT_1:55;
then A10: x in dom (f * ((canon_image X,1) " )) by A9, RELAT_1:46;
dom f c= X ;
then dom f c= dom (canon_image X,1) by Lm2;
then A11: dom f c= rng ((canon_image X,1) " ) by FUNCT_1:55;
rng f c= Y ;
then A12: rng (f * ((canon_image X,1) " )) c= Y by A11, RELAT_1:47;
then rng (f * ((canon_image X,1) " )) c= dom (canon_image Y,1) by Lm2;
then x in dom ((canon_image Y,1) * (f * ((canon_image X,1) " ))) by A10, RELAT_1:46;
then A13: x in dom (((canon_image Y,1) * f) * ((canon_image X,1) " )) by RELAT_1:55;
set y = (f * ((canon_image X,1) " )) . x;
free_magmaF g extends ((canon_image Z,1) * g) * ((canon_image Y,1) " ) by Def22;
then A14: ( 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 ) by Def3;
(f * ((canon_image X,1) " )) . x in rng (f * ((canon_image X,1) " )) by FUNCT_1:12, A10;
then A15: (f * ((canon_image X,1) " )) . x in Y by A12;
then A16: (f * ((canon_image X,1) " )) . x in dom (canon_image Y,1) by Lm2;
then A17: (canon_image Y,1) . ((f * ((canon_image X,1) " )) . x) in rng (canon_image Y,1) by FUNCT_1:12;
Y c= dom g by FUNCT_2:def 1;
then A18: dom (canon_image Y,1) c= dom g by Lm2;
rng g c= Z ;
then rng g c= dom (canon_image Z,1) by Lm2;
then dom (canon_image Y,1) c= dom ((canon_image Z,1) * g) by A18, RELAT_1:46;
then A19: rng ((canon_image Y,1) " ) c= dom ((canon_image Z,1) * g) by FUNCT_1:55;
rng (canon_image Y,1) c= dom ((canon_image Y,1) " ) by FUNCT_1:55;
then A20: rng (canon_image Y,1) c= dom (((canon_image Z,1) * g) * ((canon_image Y,1) " )) by A19, RELAT_1:46;
A21: rng (canon_image Y,1) c= dom ((canon_image Y,1) " ) by FUNCT_1:55;
dom (canon_image Y,1) = Y by Lm2;
then A22: (f * ((canon_image X,1) " )) . x in dom (((canon_image Y,1) " ) * (canon_image Y,1)) by A15, A21, RELAT_1:46;
A23: ((canon_image Z,1) * g) * (f * ((canon_image X,1) " )) = (canon_image Z,1) * (g * (f * ((canon_image X,1) " ))) by RELAT_1:55
.= (canon_image Z,1) * ((g * f) * ((canon_image X,1) " )) by RELAT_1:55
.= ((canon_image Z,1) * (g * f)) * ((canon_image X,1) " ) by RELAT_1:55 ;
thus ((free_magmaF g) * (free_magmaF f)) . x = (free_magmaF g) . ((free_magmaF f) . x) by A7, A6, FUNCT_1:22
.= (free_magmaF g) . ((((canon_image Y,1) * f) * ((canon_image X,1) " )) . x) by A13, A8, PARTFUN1:132
.= (free_magmaF g) . (((canon_image Y,1) * (f * ((canon_image X,1) " ))) . x) by RELAT_1:55
.= (free_magmaF g) . ((canon_image Y,1) . ((f * ((canon_image X,1) " )) . x)) by A10, FUNCT_1:23
.= (((canon_image Z,1) * g) * ((canon_image Y,1) " )) . ((canon_image Y,1) . ((f * ((canon_image X,1) " )) . x)) by A20, A17, A14, PARTFUN1:132
.= ((((canon_image Z,1) * g) * ((canon_image Y,1) " )) * (canon_image Y,1)) . ((f * ((canon_image X,1) " )) . x) by A16, FUNCT_1:23
.= (((canon_image Z,1) * g) * (((canon_image Y,1) " ) * (canon_image Y,1))) . ((f * ((canon_image X,1) " )) . x) by RELAT_1:55
.= ((canon_image Z,1) * g) . ((((canon_image Y,1) " ) * (canon_image Y,1)) . ((f * ((canon_image X,1) " )) . x)) by A22, FUNCT_1:23
.= ((canon_image Z,1) * g) . ((f * ((canon_image X,1) " )) . x) by A16, FUNCT_1:56
.= (f9 * ((canon_image X,1) " )) . x by A23, A10, FUNCT_1:23 ; :: thesis: verum

end;

then (free_magmaF g) * (free_magmaF f) tolerates f9 * ((canon_image X,1) " ) by A6, PARTFUN1:132;
then (free_magmaF g) * (free_magmaF f) extends f9 * ((canon_image X,1) " ) by A6, Def3;
hence free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f) by Def22, A4; :: thesis: verum