let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over 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 over 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 F be ManySortedFunction of U1,U2; ( 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
; 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);
H is ManySortedFunction of (Image F),U2
for
i being
object 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
object ;
( 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
;
H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)
then reconsider f =
F . i as
Function of
( the Sorts of U1 . i),
( the Sorts of U2 . i) by PBOOLE:def 15;
A3:
dom f = the
Sorts of
U1 . i
by A2, FUNCT_2:def 1;
reconsider h =
H . i as
Function of
( the Sorts of (Image F) . i),
( the Sorts of (Image F) . i) by A2, PBOOLE:def 15;
A4:
rng f c= the
Sorts of
U2 . i
by RELAT_1:def 19;
the
Sorts of
(Image F) = F .:.: the
Sorts of
U1
by A1, Def12;
then the
Sorts of
(Image F) . i =
f .: ( the Sorts of U1 . i)
by A2, PBOOLE:def 20
.=
rng f
by A3, RELAT_1:113
;
then
h is
Function of
( the Sorts of (Image F) . i),
( the Sorts of U2 . i)
by A4, FUNCT_2:7;
hence
H . i is
Function of
( the Sorts of (Image F) . i),
( the Sorts of U2 . i)
;
verum
end;
hence
H is
ManySortedFunction of
(Image F),
U2
by PBOOLE:def 15;
verum
end;
then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of (Image F),U2 ;
take
F1
; 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
; ( 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; ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus
F2 is_monomorphism Image F,U2
by Th22; F = F2 ** F1
thus
F = F2 ** F1
by Th4; verum