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 )

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

thus
( u + W = v + W implies v in u + W )
by Th44; :: thesis: verum
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

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;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 v + W or x in u + W )
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;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

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