let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
let U1, U2 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) )
assume A1:
F is_homomorphism U1,U2
; :: thesis: ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
then reconsider F1 = F as ManySortedFunction of U1,(Image F) by Lm3;
for H being ManySortedFunction of (Image F),(Image F) holds H is ManySortedFunction of (Image F),U2
proof
let H be
ManySortedFunction of
(Image F),
(Image F);
:: thesis: H is ManySortedFunction of (Image F),U2
for
i being
set st
i in the
carrier of
S holds
H . i is
Function of the
Sorts of
(Image F) . i,the
Sorts of
U2 . i
proof
let i be
set ;
:: thesis: ( i in the carrier of S implies H . i is Function of the Sorts of (Image F) . i,the Sorts of U2 . i )
assume A2:
i in the
carrier of
S
;
:: thesis: H . i is Function of the Sorts of (Image F) . i,the Sorts of U2 . i
then reconsider h =
H . i as
Function of the
Sorts of
(Image F) . i,the
Sorts of
(Image F) . i by PBOOLE:def 18;
reconsider f =
F . i as
Function of the
Sorts of
U1 . i,the
Sorts of
U2 . i by A2, PBOOLE:def 18;
( the
Sorts of
U2 . i = {} implies the
Sorts of
U1 . i = {} )
by A2;
then A3:
(
dom f = the
Sorts of
U1 . i &
rng f c= the
Sorts of
U2 . i )
by FUNCT_2:def 1, RELSET_1:12;
the
Sorts of
(Image F) = F .:.: the
Sorts of
U1
by A1, Def14;
then the
Sorts of
(Image F) . i =
f .: (the Sorts of U1 . i)
by A2, PBOOLE:def 25
.=
rng f
by A3, RELAT_1:146
;
then
h is
Function of the
Sorts of
(Image F) . i,the
Sorts of
U2 . i
by A3, FUNCT_2:9;
hence
H . i is
Function of the
Sorts of
(Image F) . i,the
Sorts of
U2 . i
;
:: thesis: verum
end;
hence
H is
ManySortedFunction of
(Image F),
U2
by PBOOLE:def 18;
:: thesis: verum
end;
then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of (Image F),U2 ;
take
F1
; :: thesis: ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
take
F2
; :: thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus
F1 is_epimorphism U1, Image F
by A1, Th20; :: thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus
F2 is_monomorphism Image F,U2
by Th22; :: thesis: F = F2 ** F1
thus
F = F2 ** F1
by Th4; :: thesis: verum