let X, Y, Z 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:7;
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;
reconsider v9 = (free_magmaF f) . a, w9 = (free_magmaF f) . b as Element of (free_magma Z) by A3;
A4: length ((free_magmaF f) . a) = ((free_magmaF f) . a) `2 by Def18
.= length v9 by Def18 ;
A5: length ((free_magmaF f) . b) = ((free_magmaF f) . b) `2 by Def18
.= length w9 by Def18 ;
thus f9 . (a * b) = ((free_magmaF f) . a) * ((free_magmaF f) . b) by GROUP_6:def 6
.= [[[(v9 `1),(w9 `1)],(v9 `2)],((length v9) + (length w9))] by Th31, A4, A5
.= (f9 . a) * (f9 . b) by Th31 ; :: thesis: verum

end;

then A6: f9 is multiplicative by GROUP_6:def 6;
rng g c= Z ;
then rng g c= dom (canon_image (Z,1)) by Lm3;
then A7: dom ((canon_image (Z,1)) * g) = dom g by RELAT_1:27;
X c= dom g by FUNCT_2:def 1;
then dom (canon_image (X,1)) c= dom ((canon_image (Z,1)) * g) by Lm3, A7;
then rng ((canon_image (X,1)) ") c= dom ((canon_image (Z,1)) * g) by FUNCT_1:33;
then A8: dom (((canon_image (Z,1)) * g) * ((canon_image (X,1)) ")) = dom ((canon_image (X,1)) ") by RELAT_1:27;
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 A8, FUNCT_1:33;
then A9: dom (((canon_image (Z,1)) * g) * ((canon_image (X,1)) ")) c= dom f9 by FUNCT_2:def 1;
for x being object 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 object ; :: 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 A10: 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 Def21;
then A11: ( 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 ) ;
rng f c= Y ;
then A12: rng f c= dom (canon_image (Y,1)) by Lm3;
rng f c= Z by A1;
then A13: rng f c= dom (canon_image (Z,1)) by Lm3;
A14: dom ((canon_image (Y,1)) * f) = dom f by A12, RELAT_1:27
.= dom ((canon_image (Z,1)) * f) by A13, RELAT_1:27 ;
for x being object 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 object ; :: thesis: ( x in dom ((canon_image (Y,1)) * f) implies ((canon_image (Y,1)) * f) . x = ((canon_image (Z,1)) * f) . x )
assume A15: x in dom ((canon_image (Y,1)) * f) ; :: thesis: ((canon_image (Y,1)) * f) . x = ((canon_image (Z,1)) * f) . x
then A16: f . x in dom (canon_image (Y,1)) by FUNCT_1:11;
then A17: f . x in Y by Lm3;
thus ((canon_image (Y,1)) * f) . x = (canon_image (Y,1)) . (f . x) by A15, FUNCT_1:12
.= [(f . x),1] by A16, Def19
.= (canon_image (Z,1)) . (f . x) by A1, A17, Lm3
.= ((canon_image (Z,1)) * f) . x by A14, A15, FUNCT_1:12 ; :: thesis: verum

end;

then (canon_image (Y,1)) * f = (canon_image (Z,1)) * g by A2, A14, FUNCT_1:2;
hence f9 . x = (((canon_image (Z,1)) * g) * ((canon_image (X,1)) ")) . x by A10, A11, PARTFUN1:53; :: thesis: verum

end;

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