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:8;

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 A2;
A13: ( dom (f * ((canon_image (X,1)) ")) c= dom g & g tolerates f * ((canon_image (X,1)) ") ) by A4;
A14: (canon_image (X,1)) . (w `1) = [(w `1),1] by A11, Lm3
.= w by Def18, A8, A10 ;
w `1 in dom (canon_image (X,1)) by A11, Lm3;
then w in rng (canon_image (X,1)) by A14, FUNCT_1:3;
then A15: w in dom ((canon_image (X,1)) ") by FUNCT_1:33;
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 w in dom (f * ((canon_image (X,1)) ")) by A15, RELAT_1:27;
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 4;
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 6;
hence h . w = g . w by A16, A3, GROUP_6:def 6; :: thesis: verum

end;

end;

end;

end;

A17: for k being Nat holds S₁[k] from NAT_1:sch 4(A5);
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;

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