let UA be Universal_Algebra; 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; ( 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
; rng h = MSAEnd (MSAlg UA)
A3:
MSAEnd (MSAlg UA) c= rng h
rng h c= MSAEnd (MSAlg UA)
proof
let x be
object ;
TARSKI:def 3 ( not x in rng h or x in MSAEnd (MSAlg UA) )
assume
x in rng h
;
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;
verum
end;
hence
rng h = MSAEnd (MSAlg UA)
by A3, XBOOLE_0:def 10; verum