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} )
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 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;
then ( a ** X = {} or a ** X = {0} ) by ZFMISC_1:33;
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 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