let K be Ring; :: thesis: for V being LeftMod of K
for a2, a1 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 a2, a1 being Vector of V
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
let a2, a1 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:43
.= (0. V) + a2 by VECTSP_1:66
.= a2 by RLVECT_1:def 7 ;
hence ( a2 in a1 + W iff a1 - a2 in W ) by VECTSP_4:76; :: thesis: verum