let X, Y, Z be non empty set ; 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; 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; 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)
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 ;
( 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)) "))
;
((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
;
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; verum