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 u, v being Element of V
for W being Subspace of V holds
( v in u + W iff u + W = v + 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 u, v being Element of V
for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let u, v be Element of V; :: thesis: for W being Subspace of V holds
( v in u + W iff u + W = v + W )
let W be Subspace of V; :: thesis: ( v in u + W iff u + W = v + W )
thus ( v in u + W implies u + W = v + W ) :: thesis: ( u + W = v + W implies v in u + W )

proof

assume v in u + W ; :: thesis: u + W = v + W
then consider z being Element of V such that
A1: v = u + z and
A2: z in W ;
thus u + W c= v + W :: according to XBOOLE_0:def 10 :: thesis: v + W c= u + W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in u + W or x in v + W )
assume x in u + W ; :: thesis: x in v + W
then consider v1 being Element of V such that
A3: x = u + v1 and
A4: v1 in W ;
v - z = u + (z - z) by A1, RLVECT_1:def 3
.= u + (0. V) by VECTSP_1:19
.= u by RLVECT_1:4 ;
then A5: x = v + (v1 + (- z)) by A3, RLVECT_1:def 3
.= v + (v1 - z) ;
v1 - z in W by A2, A4, Th23;
hence x in v + W by A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in v + W or x in u + W )
assume x in v + W ; :: thesis: x in u + W
then consider v2 being Element of V such that
A6: ( x = v + v2 & v2 in W ) ;
( z + v2 in W & x = u + (z + v2) ) by A1, A2, A6, Th20, RLVECT_1:def 3;
hence x in u + W ; :: thesis: verum

end;

thus ( u + W = v + W implies v in u + W ) by Th44; :: thesis: verum