let S be non empty non void ManySortedSign ; :: thesis:
let U1, U2 be non-empty MSAlgebra of S; :: thesis:
let F be ManySortedFunction of U1,U2; :: thesis:
let G be ManySortedFunction of U1,(Image F); :: thesis:
assume that
A1: F = G and
A2: F is_homomorphism U1,U2 ; :: thesis:
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)

set IF = Image F;
reconsider SIF = the Sorts of (Image F) as V2() MSSubset of U2 by MSUALG_2:def 10;
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
let o be OperSymbol of S; :: thesis:
assume Args o,U1 <> {} ; :: thesis:
let x be Element of Args o,U1; :: thesis:
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 4;
then A5: 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 A4, PARTFUN1:def 4;
then A6: dom (SIF * (the_arity_of o)) = dom (the Sorts of U2 * (the_arity_of o)) by A5, RELAT_1:46;
A7: 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

let x be set ; :: thesis:
assume A8: x in dom (SIF * (the_arity_of o)) ; :: thesis:
then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def 5;
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, Def14;
then (SIF * (the_arity_of o)) . x = (F .:.: the Sorts of U1) . k by A8, FUNCT_1:22
.= (F . k) .: (the Sorts of U1 . k) by PBOOLE:def 25
.= rng (F . k) by A9, RELAT_1:146 ;
hence (SIF * (the_arity_of o)) . x c= (the Sorts of U2 * (the_arity_of o)) . x by A6, A8, A10, FUNCT_1:22; :: thesis:

end;

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

A12: now

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

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:9;
then A14: (G . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (G # x) by A1, A2, Def9;
SIF is opers_closed by MSUALG_2:def 10;
then A15: SIF is_closed_on o by MSUALG_2:def 7;
( 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:10;
then Args o,(Image F) c= Args o,U2 by A6, A7, CARD_3:38;
then G # x in dom (Den o,U2) by A3, TARSKI:def 3;
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 9, XBOOLE_0:def 4;
the Charact of (Image F) = Opers U2,SIF by MSUALG_2:def 10;
then Den o,(Image F) = (Opers U2,SIF) . o by MSUALG_1:def 11
.= o /. SIF by MSUALG_2:def 9
.= (Den o,U2) | (((SIF # ) * the Arity of S) . o) by A15, MSUALG_2:def 8 ;
hence (G . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,(Image F)) . (G # x) by A14, A16, FUNCT_1:71; :: thesis:

end;

then A17: 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

let i be set ; :: thesis:
assume i in the carrier of S ; :: thesis:
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, Def14;
then A18: 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 A18, RELAT_1:146; :: thesis:

end;

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