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