let K be Ring; :: thesis: for V being LeftMod of K

for a1, a2 being Vector of V

for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let V be LeftMod of K; :: thesis: for a1, a2 being Vector of V

for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let a1, a2 be Vector of V; :: thesis: for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let W be Subspace of V; :: thesis: ( a2 in a1 + W iff a1 - a2 in W )

a1 - (a1 - a2) = (a1 - a1) + a2 by RLVECT_1:29

.= (0. V) + a2 by VECTSP_1:19

.= a2 by RLVECT_1:def 4 ;

hence ( a2 in a1 + W iff a1 - a2 in W ) by VECTSP_4:61; :: thesis: verum

for a1, a2 being Vector of V

for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let V be LeftMod of K; :: thesis: for a1, a2 being Vector of V

for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let a1, a2 be Vector of V; :: thesis: for W being Subspace of V holds

( a2 in a1 + W iff a1 - a2 in W )

let W be Subspace of V; :: thesis: ( a2 in a1 + W iff a1 - a2 in W )

a1 - (a1 - a2) = (a1 - a1) + a2 by RLVECT_1:29

.= (0. V) + a2 by VECTSP_1:19

.= a2 by RLVECT_1:def 4 ;

hence ( a2 in a1 + W iff a1 - a2 in W ) by VECTSP_4:61; :: thesis: verum