let V be RealLinearSpace; :: thesis: for v being VECTOR of V

for A being Subset of V st v + A is affinely-independent holds

A is affinely-independent

let v be VECTOR of V; :: thesis: for A being Subset of V st v + A is affinely-independent holds

A is affinely-independent

let A be Subset of V; :: thesis: ( v + A is affinely-independent implies A is affinely-independent )

assume A1: v + A is affinely-independent ; :: thesis: A is affinely-independent

(- v) + (v + A) = ((- v) + v) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

hence A is affinely-independent by A1; :: thesis: verum

for A being Subset of V st v + A is affinely-independent holds

A is affinely-independent

let v be VECTOR of V; :: thesis: for A being Subset of V st v + A is affinely-independent holds

A is affinely-independent

let A be Subset of V; :: thesis: ( v + A is affinely-independent implies A is affinely-independent )

assume A1: v + A is affinely-independent ; :: thesis: A is affinely-independent

(- v) + (v + A) = ((- v) + v) + A by Th5

.= (0. V) + A by RLVECT_1:5

.= A by Th6 ;

hence A is affinely-independent by A1; :: thesis: verum