let X be real-membered set ; :: thesis: for a being Real 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; :: 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} )

A4: a ** X = {0} and

A5: a <> 0 ; :: thesis: X = {0}

X,a ** X are_equipotent by A5, Th3;

then consider x being object such that

A6: X = {x} by A4, CARD_1:28;

A7: x in X by A6, TARSKI:def 1;

then reconsider x = x as Real ;

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

( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) )

let a be Real; :: 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
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

hence {0} c= a ** X by A2, INTEGRA2:7; :: thesis: verum

end;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

then
( a ** X = {} or a ** X = {0} )
by ZFMISC_1:33;
let i be object ; :: 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 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;assume A3: i in a ** X ; :: thesis: i in {0}

then reconsider i = i as Real ;

ex x being Complex st

( i = a * x & x in X ) by A3, MEMBER_1:195;

hence i in {0} by A1, TARSKI:def 1; :: thesis: verum

hence {0} c= a ** X by A2, INTEGRA2:7; :: thesis: verum

A4: a ** X = {0} and

A5: a <> 0 ; :: thesis: X = {0}

X,a ** X are_equipotent by A5, Th3;

then consider x being object such that

A6: X = {x} by A4, CARD_1:28;

A7: x in X by A6, TARSKI:def 1;

then reconsider x = x as Real ;

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