let S1 be OrderSortedSign; for U1, U2 being non-empty OSAlgebra of non-empty
for F being ManySortedFunction of ,U1 st F is_homomorphism U1,U2 & F is order-sorted holds
ex F1 being ManySortedFunction of ,U1 ex F2 being ManySortedFunction of ,(Image F) 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 non-empty ; for F being ManySortedFunction of ,U1 st F is_homomorphism U1,U2 & F is order-sorted holds
ex F1 being ManySortedFunction of ,U1 ex F2 being ManySortedFunction of ,(Image F) 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; ( F is_homomorphism U1,U2 & F is order-sorted implies ex F1 being ManySortedFunction of ,U1 ex F2 being ManySortedFunction of ,(Image F) 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 ex F2 being ManySortedFunction of ,(Image F) 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) holds H is ManySortedFunction of ,(Image F)
proof
let H be
ManySortedFunction of ,
(Image F);
H is ManySortedFunction of ,(Image F)
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 18;
reconsider h =
H . i as
Function of the
Sorts of
(Image F) . i,the
Sorts of
(Image F) . i by A3, PBOOLE:def 18;
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 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
;
verum
end;
hence
H is
ManySortedFunction of ,
(Image F)
by PBOOLE:def 18;
verum
end;
then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of ,(Image F) ;
consider F1 being ManySortedFunction of ,U1 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) 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