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

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