let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let W be Subspace of V; :: thesis: for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let v be VECTOR of V; :: thesis: for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let x be set ; :: thesis: ( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
thus ( x in v + W implies ex u being VECTOR of V st
( u in W & x = v + u ) ) :: thesis: ( ex u being VECTOR of V st
( u in W & x = v + u ) implies x in v + W )

proof

assume x in v + W ; :: thesis: ex u being VECTOR of V st
( u in W & x = v + u )
then x in { (v + u) where u is VECTOR of V : u in W } by RUSUB_1:def 4;
then consider u being VECTOR 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;

given u being VECTOR of V such that A2: ( u in W & x = v + u ) ; :: thesis: x in v + W
x in { (v + v1) where v1 is VECTOR of V : v1 in W } by A2;
hence x in v + W by RUSUB_1:def 4; :: thesis: verum