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 ;
then card a < 1 + 1 by ;
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 ;
A8: card (r * A) c= card A by Lm4;
(1 / r) * r = 1 by ;
then card A c= card (r * A) by ;
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 ;
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 ;
hence card A = card (r * A) by ; :: thesis: verum
end;
end;