let X be real-membered set ; :: thesis: for a being real number holds
( ( a = 0 & not X is empty implies a ** X = {0 } ) & ( not a ** X = {0 } or a = 0 or X = {0 } ) )
let a be real number ; :: thesis: ( ( a = 0 & not X is empty implies a ** X = {0 } ) & ( not a ** X = {0 } or a = 0 or X = {0 } ) )
thus ( a = 0 & not X is empty implies a ** X = {0 } ) :: thesis: ( not a ** X = {0 } or a = 0 or X = {0 } )

proof

assume that
A1: a = 0 and
A2: not X is empty ; :: thesis: a ** X = {0 }
thus a ** X c= {0 } :: according to XBOOLE_0:def 10 :: thesis: {0 } c= a ** X

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in a ** X or i in {0 } )
assume A3: i in a ** X ; :: thesis: i in {0 }
then reconsider i = i as Real ;
ex x being Element of COMPLEX st
( i = a * x & x in X ) by A3, MEMBER_1:195;
hence i in {0 } by A1, TARSKI:def 1; :: thesis: verum

end;

then ( a ** X = {} or a ** X = {0 } ) by ZFMISC_1:39;
hence {0 } c= a ** X by A2, INTEGRA2:7; :: thesis: verum

end;

assume that
A4: a ** X = {0 } and
A5: a <> 0 ; :: thesis: X = {0 }
X,a ** X are_equipotent by A5, Th3;
then consider x being set such that
A6: X = {x} by A4, CARD_1:48;
A7: x in X by A6, TARSKI:def 1;
then reconsider x = x as real number ;
reconsider x9 = x as Real by XREAL_0:def 1;
a * x in a ** X by A7, MEMBER_1:193;
then a * x = 0 by A4, TARSKI:def 1;
hence X = {0 } by A5, A6, XCMPLX_1:6; :: thesis: verum