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