let S1 be OrderSortedSign; 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; 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; ( 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 that
A1:
F is_homomorphism U1,U2
and
A2:
F is order-sorted
; 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 )
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
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 ;
( 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
;
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;
reconsider h =
H . i as
Function of
( the Sorts of (Image F) . i),
( the Sorts of (Image F) . i) by A3, PBOOLE:def 15;
A4:
dom f = the
Sorts of
U1 . i
by A3, FUNCT_2:def 1;
the
Sorts of
(Image F) = F .:.: the
Sorts of
U1
by A1, MSUALG_3:def 12;
then the
Sorts of
(Image F) . i =
f .: ( the Sorts of U1 . i)
by A3, PBOOLE:def 20
.=
rng f
by A4, RELAT_1:113
;
then
h is
Function of
( the Sorts of (Image F) . i),
( the Sorts of U2 . i)
by 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 ;
consider F1 being ManySortedFunction of U1,(Image F) such that
A5:
( F1 = F & F1 is order-sorted )
and
A6:
F1 is_epimorphism U1, Image F
by A1, A2, Th16;
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 & F1 is order-sorted & F2 is order-sorted )
take
F2
; ( 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 A6; ( 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; ( F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus
( F = F2 ** F1 & F1 is order-sorted )
by A5, MSUALG_3:4; F2 is order-sorted
Image F is order-sorted
by A1, A2, Th12;
then
the Sorts of (Image F) is OrderSortedSet of S1
by OSALG_1:17;
hence
F2 is order-sorted
; verum