let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let G be ManySortedFunction of U1,(Image F); :: thesis: ( F = G & F is_homomorphism U1,U2 implies G is_epimorphism U1, Image F )
assume that
A1: F = G and
A2: F is_homomorphism U1,U2 ; :: thesis: G is_epimorphism U1, Image F
for o being OperSymbol of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)

proof

set IF = Image F;
reconsider SIF = the Sorts of (Image F) as non-empty MSSubset of U2 by MSUALG_2:def 9;
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
let o be OperSymbol of S; :: thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) )
assume Args (o,U1) <> {} ; :: thesis: for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)
let x be Element of Args (o,U1); :: thesis: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)
set SIFo = SIF * (the_arity_of o);
set Uo = the Sorts of U2 * (the_arity_of o);
set ao = the_arity_of o;
A3: dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def 1;
A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
then rng (the_arity_of o) c= dom SIF by PARTFUN1:def 2;
then A5: dom (SIF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def 2;
then A6: dom (SIF * (the_arity_of o)) = dom ( the Sorts of U2 * (the_arity_of o)) by A5, RELAT_1:27;
A7: for x being object st x in dom (SIF * (the_arity_of o)) holds
(SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x

proof

let x be object ; :: thesis: ( x in dom (SIF * (the_arity_of o)) implies (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x )
assume A8: x in dom (SIF * (the_arity_of o)) ; :: thesis: (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x
then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def 3;
then reconsider k = (the_arity_of o) . x as Element of S by A4;
set f = F . k;
A9: dom (F . k) = the Sorts of U1 . k by FUNCT_2:def 1;
A10: rng (F . k) c= the Sorts of U2 . k by RELAT_1:def 19;
SIF = F .:.: the Sorts of U1 by A2, Def12;
then (SIF * (the_arity_of o)) . x = (F .:.: the Sorts of U1) . k by A8, FUNCT_1:12
.= (F . k) .: ( the Sorts of U1 . k) by PBOOLE:def 20
.= rng (F . k) by A9, RELAT_1:113 ;
hence (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x by A6, A8, A10, FUNCT_1:12; :: thesis: verum

end;

A11: dom x = dom (the_arity_of o) by Th6;

A12: now :: thesis: for a being object st a in dom (the_arity_of o) holds
(G # x) . a = (G1 # x) . a

let a be object ; :: thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a )
assume A13: a in dom (the_arity_of o) ; :: thesis: (G # x) . a = (G1 # x) . a
then reconsider n = a as Nat ;
(G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A11, A13, Def6;
hence (G # x) . a = (G1 # x) . a by A11, A13, Def6; :: thesis: verum

end;

( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6;
then G # x = G1 # x by A12, FUNCT_1:2;
then A14: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (G # x) by A1, A2;
SIF is opers_closed by MSUALG_2:def 9;
then A15: SIF is_closed_on o ;
( Args (o,(Image F)) = product (SIF * (the_arity_of o)) & Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) ) by PRALG_2:3;
then Args (o,(Image F)) c= Args (o,U2) by A6, A7, CARD_3:27;
then G # x in dom (Den (o,U2)) by A3;
then A16: ( ((SIF #) * the Arity of S) . o = Args (o,(Image F)) & G # x in (dom (Den (o,U2))) /\ (Args (o,(Image F))) ) by MSUALG_1:def 4, XBOOLE_0:def 4;
the Charact of (Image F) = Opers (U2,SIF) by MSUALG_2:def 9;
then Den (o,(Image F)) = (Opers (U2,SIF)) . o by MSUALG_1:def 6
.= o /. SIF by MSUALG_2:def 8
.= (Den (o,U2)) | (((SIF #) * the Arity of S) . o) by A15, MSUALG_2:def 7 ;
hence (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) by A14, A16, FUNCT_1:48; :: thesis: verum

end;

then A17: G is_homomorphism U1, Image F ;
for i being set st i in the carrier of S holds
rng (G . i) = the Sorts of (Image F) . i

proof

let i be set ; :: thesis: ( i in the carrier of S implies rng (G . i) = the Sorts of (Image F) . i )
assume i in the carrier of S ; :: thesis: rng (G . i) = the Sorts of (Image F) . i
then reconsider i = i as Element of S ;
set g = G . i;
the Sorts of (Image F) = G .:.: the Sorts of U1 by A1, A2, Def12;
then A18: the Sorts of (Image F) . i = (G . i) .: ( the Sorts of U1 . i) by PBOOLE:def 20;
dom (G . i) = the Sorts of U1 . i by FUNCT_2:def 1;
hence rng (G . i) = the Sorts of (Image F) . i by A18, RELAT_1:113; :: thesis: verum

end;

then G is "onto" ;
hence G is_epimorphism U1, Image F by A17; :: thesis: verum