let V be ComplexLinearSpace; :: thesis: for u, v being VECTOR of V
for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let u, v be VECTOR of V; :: thesis: for W being Subspace of V st u in v + W & u in (- v) + W holds
v in W
let W be Subspace of V; :: thesis: ( u in v + W & u in (- v) + W implies v in W )
assume ( u in v + W & u in (- v) + W ) ; :: thesis: v in W
then v + W = (- v) + W by Th76;
hence v in W by Th75; :: thesis: verum