let X be non empty set ; 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 ; 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; 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; ( 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
; ( 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)) ")
; ( not g is multiplicative or not g extends f * ((canon_image (X,1)) ") or h = g )
assume A3:
g is multiplicative
; ( not g extends f * ((canon_image (X,1)) ") or h = g )
assume A4:
g extends f * ((canon_image (X,1)) ")
; h = g
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A6:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]
thus
for
w being
Element of
(free_magma X) st
length w = k holds
h . w = g . w
verumproof
let w be
Element of
(free_magma X);
( length w = k implies h . w = g . w )
assume A7:
length w = k
;
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
;
h . w = g . wset 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
;
verum end; end;
end;
end;
A17:
for k being Nat holds S1[k]
from NAT_1:sch 4(A5);
for w being Element of (free_magma X) holds h . w = g . w
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; verum