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