let x be object ; :: thesis: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

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 v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

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 v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

let v be Element of V; :: thesis: for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

let W be Subspace of V; :: thesis: ( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

thus ( x in v + W implies ex u being Element of V st

( u in W & x = v + u ) ) :: thesis: ( ex u being Element of V st

( u in W & x = v + u ) implies x in v + W )

thus x in v + W by A2; :: thesis: verum

for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

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 v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

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 v being Element of V

for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

let v be Element of V; :: thesis: for W being Subspace of V holds

( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

let W be Subspace of V; :: thesis: ( x in v + W iff ex u being Element of V st

( u in W & x = v + u ) )

thus ( x in v + W implies ex u being Element of V st

( u in W & x = v + u ) ) :: thesis: ( ex u being Element of V st

( u in W & x = v + u ) implies x in v + W )

proof

given u being Element of V such that A2:
( u in W & x = v + u )
; :: thesis: x in v + W
assume
x in v + W
; :: thesis: ex u being Element of V st

( u in W & x = v + u )

then consider u being Element of V such that

A1: ( x = v + u & u in W ) ;

take u ; :: thesis: ( u in W & x = v + u )

thus ( u in W & x = v + u ) by A1; :: thesis: verum

end;( u in W & x = v + u )

then consider u being Element of V such that

A1: ( x = v + u & u in W ) ;

take u ; :: thesis: ( u in W & x = v + u )

thus ( u in W & x = v + u ) by A1; :: thesis: verum

thus x in v + W by A2; :: thesis: verum