let K be Ring; :: thesis: for V being LeftMod of
for a2, a1 being Vector of
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
let V be LeftMod of ; :: thesis: for a2, a1 being Vector of
for W being Subspace of V holds
( a2 in a1 + W iff a1 - a2 in W )
let a2, a1 be Vector of ; :: 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