let S be non empty non void ManySortedSign ; :: thesis: for U0, U1 being non-empty MSAlgebra of S
for W being strict non-empty free MSAlgebra of S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let U0, U1 be non-empty MSAlgebra of S; :: thesis: for W being strict non-empty free MSAlgebra of S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let W be strict non-empty free MSAlgebra of S; :: thesis: for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let F be ManySortedFunction of U0,U1; :: thesis: ( F is_epimorphism U0,U1 implies for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H ) )
assume A1:
F is_epimorphism U0,U1
; :: thesis: for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let G be ManySortedFunction of W,U1; :: thesis: ( G is_homomorphism W,U1 implies ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H ) )
assume A2:
G is_homomorphism W,U1
; :: thesis: ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
consider Gen being GeneratorSet of W such that
A3:
Gen is free
by MSAFREE:def 6;
set sU0 = the Sorts of U0;
set sU1 = the Sorts of U1;
set I = the carrier of S;
defpred S1[ set , set , set ] means ex f being Function of the Sorts of U0 . $3,the Sorts of U1 . $3 ex g being Function of Gen . $3,the Sorts of U1 . $3 st
( f = F . $3 & g = (G || Gen) . $3 & $1 in f " {(g . $2)} );
A4:
for i being set st i in the carrier of S holds
for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
proof
let i be
set ;
:: thesis: ( i in the carrier of S implies for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] ) )
assume A5:
i in the
carrier of
S
;
:: thesis: for x being set st x in Gen . i holds
ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
let x be
set ;
:: thesis: ( x in Gen . i implies ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] ) )
assume A6:
x in Gen . i
;
:: thesis: ex y being set st
( y in the Sorts of U0 . i & S1[y,x,i] )
reconsider f =
F . i as
Function of the
Sorts of
U0 . i,the
Sorts of
U1 . i by A5, PBOOLE:def 18;
reconsider g =
(G || Gen) . i as
Function of
Gen . i,the
Sorts of
U1 . i by A5, PBOOLE:def 18;
the
Sorts of
U1 . i <> {}
by A5;
then A7:
g . x in the
Sorts of
U1 . i
by A6, FUNCT_2:7;
F is
"onto"
by A1, MSUALG_3:def 10;
then
rng (F . i) = the
Sorts of
U1 . i
by A5, MSUALG_3:def 3;
then
f " {(g . x)} <> {}
by A7, FUNCT_2:49;
then consider y being
set such that A8:
y in f " {(g . x)}
by XBOOLE_0:def 1;
take
y
;
:: thesis: ( y in the Sorts of U0 . i & S1[y,x,i] )
thus
y in the
Sorts of
U0 . i
by A8;
:: thesis: S1[y,x,i]
thus
ex
f being
Function of the
Sorts of
U0 . i,the
Sorts of
U1 . i ex
g being
Function of
Gen . i,the
Sorts of
U1 . i st
(
f = F . i &
g = (G || Gen) . i &
y in f " {(g . x)} )
by A8;
:: thesis: verum
end;
consider H being ManySortedFunction of Gen,the Sorts of U0 such that
A9:
for i being set st i in the carrier of S holds
ex h being Function of Gen . i,the Sorts of U0 . i st
( h = H . i & ( for x being set st x in Gen . i holds
S1[h . x,x,i] ) )
from MSSUBFAM:sch 1(A4);
consider H1 being ManySortedFunction of W,U0 such that
A10:
H1 is_homomorphism W,U0
and
A11:
H1 || Gen = H
by A3, MSAFREE:def 5;
take
H1
; :: thesis: ( H1 is_homomorphism W,U0 & G = F ** H1 )
thus
H1 is_homomorphism W,U0
by A10; :: thesis: G = F ** H1
now let i be
set ;
:: thesis: ( i in the carrier of S implies (G || Gen) . i = (F ** H) . i )assume A12:
i in the
carrier of
S
;
:: thesis: (G || Gen) . i = (F ** H) . ithen A13:
( the
Sorts of
U0 . i = {} implies
Gen . i = {} )
;
reconsider f' =
F . i as
Function of the
Sorts of
U0 . i,the
Sorts of
U1 . i by A12, PBOOLE:def 18;
reconsider g' =
(G || Gen) . i as
Function of
Gen . i,the
Sorts of
U1 . i by A12, PBOOLE:def 18;
consider h being
Function of
Gen . i,the
Sorts of
U0 . i such that A14:
h = H . i
and A15:
for
x being
set st
x in Gen . i holds
ex
f being
Function of the
Sorts of
U0 . i,the
Sorts of
U1 . i ex
g being
Function of
Gen . i,the
Sorts of
U1 . i st
(
f = F . i &
g = (G || Gen) . i &
h . x in f " {(g . x)} )
by A9, A12;
A16:
the
Sorts of
U1 . i <> {}
by A12;
then A17:
Gen . i = dom g'
by FUNCT_2:def 1;
f' * h is
Function of
Gen . i,the
Sorts of
U1 . i
by A13, FUNCT_2:19;
then A18:
Gen . i = dom (f' * h)
by A16, FUNCT_2:def 1;
then
g' = f' * h
by A17, A18, FUNCT_1:9;
hence
(G || Gen) . i = (F ** H) . i
by A12, A14, MSUALG_3:2;
:: thesis: verum end;
then
G || Gen = F ** (H1 || Gen)
by A11, PBOOLE:3;
then A21:
G || Gen = (F ** H1) || Gen
by EXTENS_1:8;
F is_homomorphism U0,U1
by A1, MSUALG_3:def 10;
then
F ** H1 is_homomorphism W,U1
by A10, MSUALG_3:10;
hence
G = F ** H1
by A2, A21, EXTENS_1:23; :: thesis: verum