let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for v1, v2 being Element of V
for W being Subspace of V holds
( ex v being Element of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for v1, v2 being Element of V
for W being Subspace of V holds
( ex v being Element of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let v1, v2 be Element of V; :: thesis: for W being Subspace of V holds
( ex v being Element of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
let W be Subspace of V; :: thesis: ( ex v being Element of V st
( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )
thus ( ex v being Element of V st
( v1 in v + W & v2 in v + W ) implies v1 - v2 in W ) :: thesis: ( v1 - v2 in W implies ex v being Element of V st
( v1 in v + W & v2 in v + W ) ) assume v1 - v2 in W ; :: thesis: ex v being Element of V st
( v1 in v + W & v2 in v + W )
then A7: - (v1 - v2) in W by Th22;
take v1 ; :: thesis: ( v1 in v1 + W & v2 in v1 + W )
thus v1 in v1 + W by Th44; :: thesis: v2 in v1 + W
v1 + (- (v1 - v2)) = v1 + ((- v1) + v2) by VECTSP_1:17
.= (v1 + (- v1)) + v2 by RLVECT_1:def 3
.= (0. V) + v2 by RLVECT_1:5
.= v2 by RLVECT_1:4 ;
hence v2 in v1 + W by A7; :: thesis: verum