let S1 be OrderSortedSign; :: thesis: for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted )
let U1, U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted ) )
assume A1:
( F is_homomorphism U1,U2 & F is order-sorted )
; :: 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 & F1 is order-sorted & F2 is order-sorted )
then consider F1 being ManySortedFunction of U1,(Image F) such that
A2:
( F1 = F & F1 is order-sorted & F1 is_epimorphism U1, Image F )
by Th16;
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
S1 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 S1 implies H . i is Function of (the Sorts of (Image F) . i),(the Sorts of U2 . i) )
assume A3:
i in the
carrier of
S1
;
:: 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 A3, PBOOLE:def 18;
( the
Sorts of
U2 . i = {} implies the
Sorts of
U1 . i = {} )
by A3;
then A4:
(
dom f = the
Sorts of
U1 . i &
rng f c= the
Sorts of
U2 . i )
by FUNCT_2:def 1;
the
Sorts of
(Image F) = F .:.: the
Sorts of
U1
by A1, MSUALG_3:def 14;
then the
Sorts of
(Image F) . i =
f .: (the Sorts of U1 . i)
by A3, PBOOLE:def 25
.=
rng f
by A4, RELAT_1:146
;
then
h is
Function of
(the Sorts of (Image F) . i),
(the Sorts of U2 . i)
by 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 & F1 is order-sorted & F2 is order-sorted )
take
F2
; :: thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus
F1 is_epimorphism U1, Image F
by A2; :: thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus
F2 is_monomorphism Image F,U2
by MSUALG_3:22; :: thesis: ( F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus
( F = F2 ** F1 & F1 is order-sorted )
by A2, MSUALG_3:4; :: thesis: F2 is order-sorted
Image F is order-sorted
by A1, Th12;
then
the Sorts of (Image F) is OrderSortedSet of
by OSALG_1:17;
hence
F2 is order-sorted
; :: thesis: verum