let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds

h . x = 0 .--> x ) holds

rng h = MSAEnd (MSAlg UA)

let h be Function; :: thesis: ( dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds

h . x = 0 .--> x ) implies rng h = MSAEnd (MSAlg UA) )

assume that

A1: dom h = UAEnd UA and

A2: for x being object st x in UAEnd UA holds

h . x = 0 .--> x ; :: thesis: rng h = MSAEnd (MSAlg UA)

A3: MSAEnd (MSAlg UA) c= rng h

h . x = 0 .--> x ) holds

rng h = MSAEnd (MSAlg UA)

let h be Function; :: thesis: ( dom h = UAEnd UA & ( for x being object st x in UAEnd UA holds

h . x = 0 .--> x ) implies rng h = MSAEnd (MSAlg UA) )

assume that

A1: dom h = UAEnd UA and

A2: for x being object st x in UAEnd UA holds

h . x = 0 .--> x ; :: thesis: rng h = MSAEnd (MSAlg UA)

A3: MSAEnd (MSAlg UA) c= rng h

proof

rng h c= MSAEnd (MSAlg UA)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MSAEnd (MSAlg UA) or x in rng h )

assume A4: x in MSAEnd (MSAlg UA) ; :: thesis: x in rng h

then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Def4;

the carrier of (MSSign UA) = {0} by MSUALG_1:def 8;

then A5: f = 0 .--> (f . 0) by AUTALG_1:11;

A6: f is_homomorphism MSAlg UA, MSAlg UA by A4, Def4;

ex q being set st

( q in dom h & x = h . q )

end;assume A4: x in MSAEnd (MSAlg UA) ; :: thesis: x in rng h

then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Def4;

the carrier of (MSSign UA) = {0} by MSUALG_1:def 8;

then A5: f = 0 .--> (f . 0) by AUTALG_1:11;

A6: f is_homomorphism MSAlg UA, MSAlg UA by A4, Def4;

ex q being set st

( q in dom h & x = h . q )

proof

hence
x in rng h
by FUNCT_1:def 3; :: thesis: verum
take q = f . 0; :: thesis: ( q in dom h & x = h . q )

f is ManySortedFunction of (MSAlg UA),((MSAlg UA) Over (MSSign UA)) by MSUHOM_1:9;

then reconsider q9 = q as Function of UA,UA by AUTALG_1:31;

MSAlg q9 = f by A5, MSUHOM_1:def 3;

then MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A6, MSUHOM_1:9;

then q9 is_homomorphism by MSUHOM_1:21;

hence q in dom h by A1, Def1; :: thesis: x = h . q

hence x = h . q by A1, A2, A5; :: thesis: verum

end;f is ManySortedFunction of (MSAlg UA),((MSAlg UA) Over (MSSign UA)) by MSUHOM_1:9;

then reconsider q9 = q as Function of UA,UA by AUTALG_1:31;

MSAlg q9 = f by A5, MSUHOM_1:def 3;

then MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A6, MSUHOM_1:9;

then q9 is_homomorphism by MSUHOM_1:21;

hence q in dom h by A1, Def1; :: thesis: x = h . q

hence x = h . q by A1, A2, A5; :: thesis: verum

proof

hence
rng h = MSAEnd (MSAlg UA)
by A3, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng h or x in MSAEnd (MSAlg UA) )

assume x in rng h ; :: thesis: x in MSAEnd (MSAlg UA)

then consider q being object such that

A7: q in dom h and

A8: x = h . q by FUNCT_1:def 3;

consider q9 being Element of UAEnd UA such that

A9: q9 = q by A1, A7;

( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A7, A8, Th12;

then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that

A10: d = x ;

q9 is_homomorphism by Def1;

then A11: MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16;

MSAlg q9 = 0 .--> q by A9, MSUHOM_1:def 3

.= x by A1, A2, A7, A8 ;

then d is_homomorphism MSAlg UA, MSAlg UA by A10, A11, MSUHOM_1:9;

hence x in MSAEnd (MSAlg UA) by A10, Def4; :: thesis: verum

end;assume x in rng h ; :: thesis: x in MSAEnd (MSAlg UA)

then consider q being object such that

A7: q in dom h and

A8: x = h . q by FUNCT_1:def 3;

consider q9 being Element of UAEnd UA such that

A9: q9 = q by A1, A7;

( x = 0 .--> q & 0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) ) by A1, A2, A7, A8, Th12;

then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that

A10: d = x ;

q9 is_homomorphism by Def1;

then A11: MSAlg q9 is_homomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:16;

MSAlg q9 = 0 .--> q by A9, MSUHOM_1:def 3

.= x by A1, A2, A7, A8 ;

then d is_homomorphism MSAlg UA, MSAlg UA by A10, A11, MSUHOM_1:9;

hence x in MSAEnd (MSAlg UA) by A10, Def4; :: thesis: verum