let K be Ring; :: thesis: for V being LeftMod of
for a1, a2 being Vector of
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
let V be LeftMod of ; :: thesis: for a1, a2 being Vector of
for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
let a1, a2 be Vector of ; :: thesis: for W being Subspace of V holds
( a1 + W = a2 + W iff a1 - a2 in W )
let W be Subspace of V; :: thesis: ( a1 + W = a2 + W iff a1 - a2 in W )
( a2 in a1 + W iff a1 + W = a2 + W ) by VECTSP_4:70;
hence ( a1 + W = a2 + W iff a1 - a2 in W ) by Th17; :: thesis: verum