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,() 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,() 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,() st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F

let G be ManySortedFunction of U1,(); :: 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 . ) . ((Den (o,U1)) . x) = (Den (o,())) . (G # x)
proof
set IF = Image F;
reconsider SIF = the Sorts of () as V2() 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 . ) . ((Den (o,U1)) . x) = (Den (o,())) . (G # x) )
assume Args (o,U1) <> {} ; :: thesis: for x being Element of Args (o,U1) holds (G . ) . ((Den (o,U1)) . x) = (Den (o,())) . (G # x)
let x be Element of Args (o,U1); :: thesis: (G . ) . ((Den (o,U1)) . x) = (Den (o,())) . (G # x)
set SIFo = SIF * ();
set Uo = the Sorts of U2 * ();
set ao = the_arity_of o;
A3: dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def 1;
A4: rng () c= the carrier of S by FINSEQ_1:def 4;
then rng () c= dom SIF by PARTFUN1:def 2;
then A5: dom (SIF * ()) = dom () by RELAT_1:27;
rng () c= dom the Sorts of U2 by ;
then A6: dom (SIF * ()) = dom ( the Sorts of U2 * ()) by ;
A7: for x being object st x in dom (SIF * ()) holds
(SIF * ()) . x c= ( the Sorts of U2 * ()) . x
proof
let x be object ; :: thesis: ( x in dom (SIF * ()) implies (SIF * ()) . x c= ( the Sorts of U2 * ()) . x )
assume A8: x in dom (SIF * ()) ; :: thesis: (SIF * ()) . x c= ( the Sorts of U2 * ()) . x
then (the_arity_of o) . x in rng () by ;
then reconsider k = () . 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 ;
then (SIF * ()) . x = (F .:.: the Sorts of U1) . k by
.= (F . k) .: ( the Sorts of U1 . k) by PBOOLE:def 20
.= rng (F . k) by ;
hence (SIF * ()) . x c= ( the Sorts of U2 * ()) . x by ; :: thesis: verum
end;
A11: dom x = dom () by Th6;
A12: now :: thesis: for a being object st a in dom () holds
(G # x) . a = (G1 # x) . a
let a be object ; :: thesis: ( a in dom () implies (G # x) . a = (G1 # x) . a )
assume A13: a in dom () ; :: thesis: (G # x) . a = (G1 # x) . a
then reconsider n = a as Nat ;
(G # x) . n = (G . (() /. n)) . (x . n) by ;
hence (G # x) . a = (G1 # x) . a by ; :: thesis: verum
end;
( dom (G # x) = dom () & dom (G1 # x) = dom () ) by Th6;
then G # x = G1 # x by ;
then A14: (G . ) . ((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,()) = product (SIF * ()) & Args (o,U2) = product ( the Sorts of U2 * ()) ) by PRALG_2:3;
then Args (o,()) c= Args (o,U2) by ;
then G # x in dom (Den (o,U2)) by A3;
then A16: ( ((SIF #) * the Arity of S) . o = Args (o,()) & G # x in (dom (Den (o,U2))) /\ (Args (o,())) ) by ;
the Charact of () = Opers (U2,SIF) by MSUALG_2:def 9;
then Den (o,()) = (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 ;
hence (G . ) . ((Den (o,U1)) . x) = (Den (o,())) . (G # x) by ; :: 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 () . i
proof
let i be set ; :: thesis: ( i in the carrier of S implies rng (G . i) = the Sorts of () . i )
assume i in the carrier of S ; :: thesis: rng (G . i) = the Sorts of () . i
then reconsider i = i as Element of S ;
set g = G . i;
the Sorts of () = G .:.: the Sorts of U1 by ;
then A18: the Sorts of () . 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 () . i by ; :: thesis: verum
end;
then G is "onto" ;
hence G is_epimorphism U1, Image F by A17; :: thesis: verum