let r be Real; :: thesis: for V being RealLinearSpace
for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
let V be RealLinearSpace; :: thesis: for A being Subset of V st r * A is affinely-independent & r <> 0 holds
A is affinely-independent
let A be Subset of V; :: thesis: ( r * A is affinely-independent & r <> 0 implies A is affinely-independent )
assume that
A1: r * A is affinely-independent and
A2: r <> 0 ; :: thesis: A is affinely-independent
(r ") * (r * A) = ((r ") * r) * A by Th10
.= 1 * A by A2, XCMPLX_0:def 7
.= A by Th11 ;
hence A is affinely-independent by A1; :: thesis: verum