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 A1: ( a = 0 & 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 A2: i in a ** X ; :: thesis: i in {0 }
then reconsider i = i as Real ;
consider x being Real such that
A3: ( x in X & i = a * x ) by A2, INTEGRA2:def 2;
thus i in {0 } by A1, A3, TARSKI:def 1; :: thesis: verum

end;

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

end;

assume A4: ( a ** X = {0 } & a <> 0 ) ; :: thesis: X = {0 }
then X,a ** X are_equipotent by Th3;
then consider x being set such that
A5: X = {x} by A4, CARD_1:48;
A6: x in X by A5, TARSKI:def 1;
then reconsider x = x as real number ;
reconsider x' = x as Real by XREAL_0:def 1;
a * x' is Real ;
then a * x in a ** X by A6, INTEGRA2:def 2;
then a * x = 0 by A4, TARSKI:def 1;
hence X = {0 } by A4, A5, XCMPLX_1:6; :: thesis: verum