let UA be Universal_Algebra; :: thesis: for h being Function st dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) holds
rng h = MSAAut (MSAlg UA)
let h be Function; :: thesis: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) implies rng h = MSAAut (MSAlg UA) )
assume A1: ( dom h = UAAut UA & ( for x being set st x in UAAut UA holds
h . x = 0 .--> x ) ) ; :: thesis: rng h = MSAAut (MSAlg UA)
thus rng h = MSAAut (MSAlg UA) :: thesis: verum

proof

thus rng h c= MSAAut (MSAlg UA) :: according to XBOOLE_0:def 10 :: thesis: MSAAut (MSAlg UA) c= rng h

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng h or x in MSAAut (MSAlg UA) )
assume x in rng h ; :: thesis: x in MSAAut (MSAlg UA)
then consider q being set such that
A2: ( q in dom h & x = h . q ) by FUNCT_1:def 5;
A3: x = 0 .--> q by A1, A2;
0 .--> q is ManySortedFunction of (MSAlg UA),(MSAlg UA) by A1, A2, Th39;
then consider d being ManySortedFunction of (MSAlg UA),(MSAlg UA) such that
A4: d = x by A3;
consider q' being Element of UAAut UA such that
A5: q' = q by A1, A2;
q' is_isomorphism UA,UA by Def1;
then A6: MSAlg q' is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by MSUHOM_1:20;
MSAlg q' = 0 .--> q by A5, MSUHOM_1:def 3
.= x by A1, A2 ;
then d is_isomorphism MSAlg UA, MSAlg UA by A4, A6, MSUHOM_1:9;
hence x in MSAAut (MSAlg UA) by A4, Def7; :: thesis: verum

end;

thus MSAAut (MSAlg UA) c= rng h :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MSAAut (MSAlg UA) or x in rng h )
assume A7: x in MSAAut (MSAlg UA) ; :: thesis: x in rng h
then reconsider f = x as ManySortedFunction of (MSAlg UA),(MSAlg UA) by Def7;
A8: f is_isomorphism MSAlg UA, MSAlg UA by A7, Def7;
reconsider g = (*--> 0 ) * (signature UA) as Function of dom (signature UA),{0 } * by MSUALG_1:7;
( the carrier of (MSSign UA) = {0 } & the carrier' of (MSSign UA) = dom (signature UA) & the Arity of (MSSign UA) = g & the ResultSort of (MSSign UA) = (dom (signature UA)) --> 0 ) by MSUALG_1:def 13;
then A9: f = 0 .--> (f . 0 ) by Th12;
ex q being set st
( q in dom h & x = h . q )

proof

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 q' = q as Function of UA,UA by Th38;
MSAlg q' = f by A9, MSUHOM_1:def 3;
then MSAlg q' is_isomorphism MSAlg UA,(MSAlg UA) Over (MSSign UA) by A8, MSUHOM_1:9;
then q' is_isomorphism UA,UA by MSUHOM_1:24;
hence q in dom h by A1, Def1; :: thesis: x = h . q
hence x = h . q by A1, A9; :: thesis: verum

end;

hence x in rng h by FUNCT_1:def 5; :: thesis: verum

end;

end;