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)

for i being set st i in the carrier of S holds

rng (G . i) = the Sorts of (Image F) . i

hence G is_epimorphism U1, Image F by A17; :: thesis: verum

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

then A17:
G is_homomorphism U1, Image F
;
set IF = Image F;

reconsider SIF = the Sorts of (Image F) 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 . (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

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;reconsider SIF = the Sorts of (Image F) 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 . (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

A11:
dom x = dom (the_arity_of o)
by Th6;
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;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

A12: now :: thesis: for a being object st a in dom (the_arity_of o) holds

(G # x) . a = (G1 # x) . a

( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) )
by Th6;(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;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

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

for i being set st i in the carrier of S holds

rng (G . i) = the Sorts of (Image F) . i

proof

then
G is "onto"
;
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;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

hence G is_epimorphism U1, Image F by A17; :: thesis: verum