let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
let X be V5() ManySortedSet of S; for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
set X0 = X;
let h be ManySortedFunction of (Free (S,X)),A; ( h is_homomorphism Free (S,X),A implies ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) ) )
assume A1:
h is_homomorphism Free (S,X),A
; ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
set ww = canonical_homomorphism A;
reconsider H = FreeGen X as GeneratorSet of Free (S,X) by Th45;
reconsider G = FreeGen X as GeneratorSet of A by Th45;
A2:
now for s being SortSymbol of S
for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]let s be
SortSymbol of
S;
for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]let i be
Element of
X . s;
((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
root-tree [i,s] in FreeGen (
s,
X)
by MSAFREE:def 15;
then A3:
root-tree [i,s] in H . s
by MSAFREE:def 16;
G c= the
Sorts of
A
by PBOOLE:def 18;
then
H . s c= the
Sorts of
A . s
;
hence
((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
by A3, Th47;
verum end;
then A4:
( canonical_homomorphism A is_homomorphism Free (S,X),A & ( for s being SortSymbol of S
for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s] ) )
by Def10;
reconsider hG = h || H as ManySortedFunction of G, the Sorts of A ;
consider g being ManySortedFunction of A,A such that
A5:
( g is_homomorphism A,A & g || G = hG )
by Def9;
take
g
; ( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
thus
g is_homomorphism A,A
by A5; h = g ** (canonical_homomorphism A)
A6:
g ** (canonical_homomorphism A) is_homomorphism Free (S,X),A
by A4, A5, MSUALG_3:10;
now for x being object st x in the carrier of S holds
(h || H) . x = ((g ** (canonical_homomorphism A)) || H) . xlet x be
object ;
( x in the carrier of S implies (h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x )assume
x in the
carrier of
S
;
(h || H) . x = ((g ** (canonical_homomorphism A)) || H) . xthen reconsider s =
x as
SortSymbol of
S ;
A7:
(
dom ((h || H) . s) = H . s &
dom (((g ** (canonical_homomorphism A)) || H) . s) = H . s )
by FUNCT_2:def 1;
now for y being object st y in H . s holds
((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . ylet y be
object ;
( y in H . s implies ((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . y )assume A8:
y in H . s
;
((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . ythen
y in FreeGen (
s,
X)
by MSAFREE:def 16;
then consider z being
set such that A9:
(
z in X . s &
y = root-tree [z,s] )
by MSAFREE:def 15;
A10:
((canonical_homomorphism A) . s) . y = root-tree [z,s]
by A2, A9;
then
((canonical_homomorphism A) . s) . y in FreeGen (
s,
X)
by A9, MSAFREE:def 15;
then A11:
((canonical_homomorphism A) . s) . y in G . s
by MSAFREE:def 16;
A12:
H . s c= the
Sorts of
(Free (S,X)) . s
by PBOOLE:def 2, PBOOLE:def 18;
A13:
dom (g ** (canonical_homomorphism A)) = the
carrier of
S /\ the
carrier of
S
by PARTFUN1:def 2;
thus ((h || H) . x) . y =
((g . s) | (G . s)) . (((canonical_homomorphism A) . s) . y)
by A9, A10, A5, MSAFREE:def 1
.=
(g . s) . (((canonical_homomorphism A) . s) . y)
by A11, FUNCT_1:49
.=
((g . s) * ((canonical_homomorphism A) . s)) . y
by A8, A12, FUNCT_2:15
.=
((g ** (canonical_homomorphism A)) . s) . y
by A13, PBOOLE:def 19
.=
(((g ** (canonical_homomorphism A)) . s) | (H . s)) . y
by A8, FUNCT_1:49
.=
(((g ** (canonical_homomorphism A)) || H) . x) . y
by MSAFREE:def 1
;
verum end; hence
(h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x
by A7;
verum end;
hence
h = g ** (canonical_homomorphism A)
by A1, A6, EXTENS_1:19, PBOOLE:3; verum