let X be non empty set ; :: thesis: for M being non empty multMagma
for f being Function of X,M
for h, g being Function of (free_magma X),M st h is multiplicative & h extends f * ((canon_image X,1) " ) & g is multiplicative & g extends f * ((canon_image X,1) " ) holds
h = g
let M be non empty multMagma ; :: thesis: for f being Function of X,M
for h, g being Function of (free_magma X),M st h is multiplicative & h extends f * ((canon_image X,1) " ) & g is multiplicative & g extends f * ((canon_image X,1) " ) holds
h = g
let f be Function of X,M; :: thesis: for h, g being Function of (free_magma X),M st h is multiplicative & h extends f * ((canon_image X,1) " ) & g is multiplicative & g extends f * ((canon_image X,1) " ) holds
h = g
let h, g be Function of (free_magma X),M; :: thesis: ( h is multiplicative & h extends f * ((canon_image X,1) " ) & g is multiplicative & g extends f * ((canon_image X,1) " ) implies h = g )
assume A1: h is multiplicative ; :: thesis: ( not h extends f * ((canon_image X,1) " ) or not g is multiplicative or not g extends f * ((canon_image X,1) " ) or h = g )
assume A2: h extends f * ((canon_image X,1) " ) ; :: thesis: ( not g is multiplicative or not g extends f * ((canon_image X,1) " ) or h = g )
assume A3: g is multiplicative ; :: thesis: ( not g extends f * ((canon_image X,1) " ) or h = g )
assume A4: g extends f * ((canon_image X,1) " ) ; :: thesis: h = g
defpred S₁[ Nat] means for w being Element of (free_magma X) st length w = $1 holds
h . w = g . w;
A5: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A6: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
thus for w being Element of (free_magma X) st length w = k holds
h . w = g . w :: thesis: verum

proof

let w be Element of (free_magma X); :: thesis: ( length w = k implies h . w = g . w )
assume A7: length w = k ; :: thesis: h . w = g . w
A8: ( w = [(w `1 ),(w `2 )] & length w >= 1 ) by Th32;
then ( length w = 1 or length w > 1 ) by XXREAL_0:1;
then A9: ( length w = 1 or (length w) + 1 > 1 + 1 ) by XREAL_1:10;

per cases ( length w = 1 or length w >= 2 ) by A9, NAT_1:13;

suppose A10: length w = 1 ; :: thesis: h . w = g . w

set x = w `1 ;
w `1 in { (w9 `1 ) where w9 is Element of (free_magma X) : length w9 = 1 } by A10;
then A11: w `1 in X by Th30;
A12: ( dom (f * ((canon_image X,1) " )) c= dom h & h tolerates f * ((canon_image X,1) " ) ) by Def3, A2;
A13: ( dom (f * ((canon_image X,1) " )) c= dom g & g tolerates f * ((canon_image X,1) " ) ) by Def3, A4;
A14: (canon_image X,1) . (w `1 ) = [(w `1 ),1] by A11, Lm2
.= w by Def19, A8, A10 ;
w `1 in dom (canon_image X,1) by A11, Lm2;
then w in rng (canon_image X,1) by A14, FUNCT_1:12;
then A15: w in dom ((canon_image X,1) " ) by FUNCT_1:55;
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 w in dom (f * ((canon_image X,1) " )) by A15, RELAT_1:46;
then ( w in (dom h) /\ (dom (f * ((canon_image X,1) " ))) & w in (dom g) /\ (dom (f * ((canon_image X,1) " ))) ) by A12, A13, XBOOLE_1:28;
then ( h . w = (f * ((canon_image X,1) " )) . w & g . w = (f * ((canon_image X,1) " )) . w ) by A12, A13, PARTFUN1:def 6;
hence h . w = g . w ; :: thesis: verum

end;

suppose length w >= 2 ; :: thesis: h . w = g . w

then consider w1, w2 being Element of (free_magma X) such that
A16: ( w = w1 * w2 & length w1 < length w & length w2 < length w ) by Th34;
( h . w1 = g . w1 & h . w2 = g . w2 ) by A6, A7, A16;
then h . (w1 * w2) = (g . w1) * (g . w2) by A1, GROUP_6:def 7;
hence h . w = g . w by A16, A3, GROUP_6:def 7; :: thesis: verum

end;

end;

end;

end;

A17: for k being Nat holds S₁[k] from NAT_1:sch 4(A5);
A18: for w being Element of (free_magma X) holds h . w = g . w

proof

let w be Element of (free_magma X); :: thesis: h . w = g . w
reconsider k = length w as Nat ;
S₁[k] by A17;
hence h . w = g . w ; :: thesis: verum

end;

for x being set st x in the carrier of (free_magma X) holds
h . x = g . x by A18;
hence h = g by FUNCT_2:18; :: thesis: verum