let V be RealLinearSpace; :: thesis: for A being Subset of V st 0. V in A holds

( A is affinely-independent iff A \ {(0. V)} is linearly-independent )

let A be Subset of V; :: thesis: ( 0. V in A implies ( A is affinely-independent iff A \ {(0. V)} is linearly-independent ) )

assume A1: 0. V in A ; :: thesis: ( A is affinely-independent iff A \ {(0. V)} is linearly-independent )

A2: (- (0. V)) + A = (0. V) + A

.= A by Th6 ;

hence ( A is affinely-independent implies A \ {(0. V)} is linearly-independent ) by A1, Th41; :: thesis: ( A \ {(0. V)} is linearly-independent implies A is affinely-independent )

assume A \ {(0. V)} is linearly-independent ; :: thesis: A is affinely-independent

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

( A is affinely-independent iff A \ {(0. V)} is linearly-independent )

let A be Subset of V; :: thesis: ( 0. V in A implies ( A is affinely-independent iff A \ {(0. V)} is linearly-independent ) )

assume A1: 0. V in A ; :: thesis: ( A is affinely-independent iff A \ {(0. V)} is linearly-independent )

A2: (- (0. V)) + A = (0. V) + A

.= A by Th6 ;

hence ( A is affinely-independent implies A \ {(0. V)} is linearly-independent ) by A1, Th41; :: thesis: ( A \ {(0. V)} is linearly-independent implies A is affinely-independent )

assume A \ {(0. V)} is linearly-independent ; :: thesis: A is affinely-independent

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