let X, Z, Y be non empty set ; :: thesis: for f being Function of X,Y
for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g
let f be Function of X,Y; :: thesis: for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g
let g be Function of X,Z; :: thesis: ( Y c= Z & f = g implies free_magmaF f = free_magmaF g )
assume A1: Y c= Z ; :: thesis: ( not f = g or free_magmaF f = free_magmaF g )
assume A2: f = g ; :: thesis: free_magmaF f = free_magmaF g
A3: the carrier of (free_magma Y) c= the carrier of (free_magma Z) by A1, Th27;
then reconsider f9 = free_magmaF f as Function of (free_magma X),(free_magma Z) by FUNCT_2:9;
for a, b being Element of (free_magma X) holds f9 . (a * b) = (f9 . a) * (f9 . b)

proof

let a, b be Element of (free_magma X); :: thesis: f9 . (a * b) = (f9 . a) * (f9 . b)
set v = (free_magmaF f) . a;
set w = (free_magmaF f) . b;
( (free_magmaF f) . a in the carrier of (free_magma Y) & (free_magmaF f) . b in the carrier of (free_magma Y) ) ;
then reconsider v9 = (free_magmaF f) . a, w9 = (free_magmaF f) . b as Element of (free_magma Z) by A3;
A5: length ((free_magmaF f) . a) = ((free_magmaF f) . a) `2 by Def19
.= length v9 by Def19 ;
A6: length ((free_magmaF f) . b) = ((free_magmaF f) . b) `2 by Def19
.= length w9 by Def19 ;
thus f9 . (a * b) = ((free_magmaF f) . a) * ((free_magmaF f) . b) by GROUP_6:def 7
.= [[[(v9 `1 ),(w9 `1 )],(v9 `2 )],((length v9) + (length w9))] by Th31, A5, A6
.= (f9 . a) * (f9 . b) by Th31 ; :: thesis: verum

end;

then A7: f9 is multiplicative by GROUP_6:def 7;
rng g c= Z ;
then rng g c= dom (canon_image Z,1) by Lm2;
then A8: dom ((canon_image Z,1) * g) = dom g by RELAT_1:46;
X c= dom g by FUNCT_2:def 1;
then dom (canon_image X,1) c= dom ((canon_image Z,1) * g) by Lm2, A8;
then rng ((canon_image X,1) " ) c= dom ((canon_image Z,1) * g) by FUNCT_1:55;
then A9: dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) = dom ((canon_image X,1) " ) by RELAT_1:46;
rng (canon_image X,1) c= the carrier of (free_magma X) ;
then dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) c= the carrier of (free_magma X) by A9, FUNCT_1:55;
then A10: dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) c= dom f9 by FUNCT_2:def 1;
for x being set st x in dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) holds
f9 . x = (((canon_image Z,1) * g) * ((canon_image X,1) " )) . x

proof

let x be set ; :: thesis: ( x in dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) implies f9 . x = (((canon_image Z,1) * g) * ((canon_image X,1) " )) . x )
assume A11: x in dom (((canon_image Z,1) * g) * ((canon_image X,1) " )) ; :: thesis: f9 . x = (((canon_image Z,1) * g) * ((canon_image X,1) " )) . x
free_magmaF f extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) by Def22;
then A12: ( 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;
rng f c= Y ;
then A13: rng f c= dom (canon_image Y,1) by Lm2;
rng f c= Z by A1, XBOOLE_1:1;
then A14: rng f c= dom (canon_image Z,1) by Lm2;
A15: dom ((canon_image Y,1) * f) = dom f by A13, RELAT_1:46
.= dom ((canon_image Z,1) * f) by A14, RELAT_1:46 ;
for x being set st x in dom ((canon_image Y,1) * f) holds
((canon_image Y,1) * f) . x = ((canon_image Z,1) * f) . x

proof

let x be set ; :: thesis: ( x in dom ((canon_image Y,1) * f) implies ((canon_image Y,1) * f) . x = ((canon_image Z,1) * f) . x )
assume A16: x in dom ((canon_image Y,1) * f) ; :: thesis: ((canon_image Y,1) * f) . x = ((canon_image Z,1) * f) . x
then A17: f . x in dom (canon_image Y,1) by FUNCT_1:21;
then A18: f . x in Y by Lm2;
thus ((canon_image Y,1) * f) . x = (canon_image Y,1) . (f . x) by A16, FUNCT_1:22
.= [(f . x),1] by A17, Def20
.= (canon_image Z,1) . (f . x) by A1, A18, Lm2
.= ((canon_image Z,1) * f) . x by A15, A16, FUNCT_1:22 ; :: thesis: verum

end;

then A19: (canon_image Y,1) * f = (canon_image Z,1) * g by A2, A15, FUNCT_1:9;
thus f9 . x = (((canon_image Z,1) * g) * ((canon_image X,1) " )) . x by A19, A11, A12, PARTFUN1:132; :: thesis: verum

end;

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