let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of 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 of 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 A1: ( F = G & 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

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)
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
A2: ( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6;
A3: dom x = dom (the_arity_of o) by Th6;

now

let a be set ; :: thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a )
assume A4: 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) & (G1 # x) . n = (G1 . ((the_arity_of o) /. n)) . (x . n) ) by A3, A4, Def8;
hence (G # x) . a = (G1 # x) . a ; :: thesis: verum

end;

then G # x = G1 # x by A2, FUNCT_1:9;
then A5: (G . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (G # x) by A1, Def9;
set IF = Image F;
reconsider SIF = the Sorts of (Image F) as V2 MSSubset of U2 by MSUALG_2:def 10;
A6: ( the Charact of (Image F) = Opers U2,SIF & SIF is opers_closed ) by MSUALG_2:def 10;
then A7: SIF is_closed_on o by MSUALG_2:def 7;
A8: Den o,(Image F) = (Opers U2,SIF) . o by A6, MSUALG_1:def 11
.= o /. SIF by MSUALG_2:def 9
.= (Den o,U2) | (((SIF # ) * the Arity of S) . o) by A7, MSUALG_2:def 8 ;
A9: ((SIF # ) * the Arity of S) . o = Args o,(Image F) by MSUALG_1:def 9;
set SIFo = SIF * (the_arity_of o);
set Uo = the Sorts of U2 * (the_arity_of o);
set ao = the_arity_of o;
A10: Args o,(Image F) = product (SIF * (the_arity_of o)) by PRALG_2:10;
A11: Args o,U2 = product (the Sorts of U2 * (the_arity_of o)) by PRALG_2:10;
A12: 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 PBOOLE:def 3;
then A13: dom (SIF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:46;
rng (the_arity_of o) c= dom the Sorts of U2 by A12, PBOOLE:def 3;
then A14: dom (SIF * (the_arity_of o)) = dom (the Sorts of U2 * (the_arity_of o)) by A13, RELAT_1:46;
for x being set 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 set ; :: 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 A15: 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 A13, FUNCT_1:def 5;
then reconsider k = (the_arity_of o) . x as Element of S by A12;
set f = F . k;
A16: ( dom (F . k) = the Sorts of U1 . k & rng (F . k) c= the Sorts of U2 . k ) by FUNCT_2:def 1, RELSET_1:12;
SIF = F .:.: the Sorts of U1 by A1, Def14;
then (SIF * (the_arity_of o)) . x = (F .:.: the Sorts of U1) . k by A15, FUNCT_1:22
.= (F . k) .: (the Sorts of U1 . k) by PBOOLE:def 25
.= rng (F . k) by A16, RELAT_1:146 ;
hence (SIF * (the_arity_of o)) . x c= (the Sorts of U2 * (the_arity_of o)) . x by A14, A15, A16, FUNCT_1:22; :: thesis: verum

end;

then A17: Args o,(Image F) c= Args o,U2 by A10, A11, A14, CARD_3:38;
dom (Den o,U2) = Args o,U2 by FUNCT_2:def 1;
then ( G # x in ((SIF # ) * the Arity of S) . o & G # x in dom (Den o,U2) ) by A9, A17, TARSKI:def 3;
then G # x in (dom (Den o,U2)) /\ (Args o,(Image F)) by XBOOLE_0:def 4;
hence (G . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(Image F)) . (G # x) by A5, A8, A9, FUNCT_1:71; :: thesis: verum

end;

then A18: G is_homomorphism U1, Image F by Def9;
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, Def14;
then A19: the Sorts of (Image F) . i = (G . i) .: (the Sorts of U1 . i) by PBOOLE:def 25;
dom (G . i) = the Sorts of U1 . i by FUNCT_2:def 1;
hence rng (G . i) = the Sorts of (Image F) . i by A19, RELAT_1:146; :: thesis: verum

end;

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