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;

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 A5:
( r <> 0 or A is trivial )
; :: thesis: 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 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

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

end;

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

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

r * A is empty

end;proof

hence
card A = card (r * A)
by A9; :: thesis: verum
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;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