let S be non empty non void ManySortedSign ; for U1, U2, U3 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra of S; for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let F be ManySortedFunction of U1,U2; for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let G be ManySortedFunction of U2,U3; ( F is_epimorphism U1,U2 & G is_epimorphism U2,U3 implies G ** F is_epimorphism U1,U3 )
assume that
A1:
F is_epimorphism U1,U2
and
A2:
G is_epimorphism U2,U3
; G ** F is_epimorphism U1,U3
A3:
G is "onto"
by A2, Def10;
A4:
F is "onto"
by A1, Def10;
for i being set st i in the carrier of S holds
rng ((G ** F) . i) = the Sorts of U3 . i
proof
let i be
set ;
( i in the carrier of S implies rng ((G ** F) . i) = the Sorts of U3 . i )
assume A5:
i in the
carrier of
S
;
rng ((G ** F) . i) = the Sorts of U3 . i
then reconsider f =
F . i as
Function of
(the Sorts of U1 . i),
(the Sorts of U2 . i) by PBOOLE:def 18;
reconsider g =
G . i as
Function of
(the Sorts of U2 . i),
(the Sorts of U3 . i) by A5, PBOOLE:def 18;
rng f = the
Sorts of
U2 . i
by A4, A5, Def3;
then A6:
dom g = rng f
by A5, FUNCT_2:def 1;
rng g = the
Sorts of
U3 . i
by A3, A5, Def3;
then
rng (g * f) = the
Sorts of
U3 . i
by A6, RELAT_1:47;
hence
rng ((G ** F) . i) = the
Sorts of
U3 . i
by A5, Th2;
verum
end;
then A7:
G ** F is "onto"
by Def3;
( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 )
by A1, A2, Def10;
then
G ** F is_homomorphism U1,U3
by Th10;
hence
G ** F is_epimorphism U1,U3
by A7, Def10; verum