let r be Real; :: thesis: for V being RealLinearSpace
for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
let V be RealLinearSpace; :: thesis: for A being Subset of V holds
( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
let A be Subset of V; :: thesis: ( card A = card (r * A) iff ( r <> 0 or A is trivial ) )
A1: card {(0. V)} = 1 by CARD_2:42;

hereby :: thesis: ( ( r <> 0 or A is trivial ) implies card A = card (r * A) )

assume A2: card A = card (r * A) ; :: thesis: ( r = 0 implies A is trivial )
assume A3: r = 0 ; :: thesis: A is trivial
then A4: r * A c= {(0. V)} by RLAFFIN1:12;
then reconsider a = A as finite set by A2;
reconsider rA = r * A as finite set by A4;
card rA <= card {(0. V)} by A3, NAT_1:43, RLAFFIN1:12;
then card a < 1 + 1 by A1, A2, NAT_1:13;
hence A is trivial by NAT_D:60; :: thesis: verum

end;

assume A5: ( r <> 0 or A is trivial ) ; :: thesis: card A = card (r * A)

per cases ( r <> 0 or A is empty or ( r = 0 & A is 1 -element ) ) by A5;

suppose A6: r <> 0 ; :: thesis: card A = card (r * A)

A7: ( 1 * A = A & ((1 / r) * r) * A = (1 / r) * (r * A) ) by RLAFFIN1:10, RLAFFIN1:11;
A8: card (r * A) c= card A by Lm4;
(1 / r) * r = 1 by A6, XCMPLX_1:87;
then card A c= card (r * A) by A7, Lm4;
hence card A = card (r * A) by A8; :: thesis: verum

end;

suppose A9: A is empty ; :: thesis: card A = card (r * A)

r * A is empty

proof

assume not r * A is empty ; :: thesis: contradiction
then consider x being object such that
A10: x in r * A ;
x in { (r * v) where v is Element of V : v in A } by A10, CONVEX1:def 1;
then ex v being Element of V st
( x = r * v & v in A ) ;
hence contradiction by A9; :: thesis: verum

end;

hence card A = card (r * A) by A9; :: thesis: verum

end;

suppose A11: ( r = 0 & A is 1 -element ) ; :: thesis: card A = card (r * A)

then consider x being object such that
A12: A = {x} by ZFMISC_1:131;
r * A = {(0. V)} by A11, CONVEX1:34;
hence card A = card (r * A) by A1, A12, CARD_2:42; :: thesis: verum

end;

end;