let C be MSAlgebra over S; :: thesis: ( C is A -Image implies C is non-empty )
assume C is A -Image ; :: thesis: C is non-empty
then consider B being non-empty MSAlgebra over S, h being ManySortedFunction of A,B such that
A1: ( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ) ;
thus the Sorts of C is V5() by A1; :: according to MSUALG_1:def 3 :: thesis: verum