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 ) )

( 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

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 ) )

proof

assume
v1 - v2 in W
; :: thesis: ex v being Element of V st
given v being Element of V such that A1:
v1 in v + W
and

A2: v2 in v + W ; :: thesis: v1 - v2 in W

consider u2 being Element of V such that

A3: u2 in W and

A4: v2 = v + u2 by A2, Th42;

consider u1 being Element of V such that

A5: u1 in W and

A6: v1 = v + u1 by A1, Th42;

v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, VECTSP_1:17

.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3

.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3

.= (u1 + (0. V)) - u2 by RLVECT_1:5

.= u1 - u2 by RLVECT_1:4 ;

hence v1 - v2 in W by A5, A3, Th23; :: thesis: verum

end;A2: v2 in v + W ; :: thesis: v1 - v2 in W

consider u2 being Element of V such that

A3: u2 in W and

A4: v2 = v + u2 by A2, Th42;

consider u1 being Element of V such that

A5: u1 in W and

A6: v1 = v + u1 by A1, Th42;

v1 - v2 = (u1 + v) + ((- v) - u2) by A6, A4, VECTSP_1:17

.= ((u1 + v) + (- v)) - u2 by RLVECT_1:def 3

.= (u1 + (v + (- v))) - u2 by RLVECT_1:def 3

.= (u1 + (0. V)) - u2 by RLVECT_1:5

.= u1 - u2 by RLVECT_1:4 ;

hence v1 - v2 in W by A5, A3, Th23; :: thesis: verum

( 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