let E be RealNormSpace; :: thesis: for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds
Y is open
let X, Y be Subset of E; :: thesis: for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds
Y is open
let v be Point of E; :: thesis: ( X is open & Y = { (x + v) where x is Point of E : x in X } implies Y is open )
assume that
A1: X is open and
A2: Y = { (x + v) where x is Point of E : x in X } ; :: thesis: Y is open
deffunc H₁( Point of E) -> Element of the carrier of E = (1 * $1) + (- v);
consider H being Function of E,E such that
A3: for p being Point of E holds H . p = H₁(p) from FUNCT_2:sch 4();
A4: dom H = the carrier of E by FUNCT_2:def 1;
for p being Point of E st p in the carrier of E holds
H /. p = (1 * p) + (- v) by A3;
then A5: H is_continuous_on the carrier of E by A4, NFCONT_1:52;
reconsider H1 = H as Function of (TopSpaceNorm E),(TopSpaceNorm E) ;
A6: H1 is continuous by A5, NORMSP_2:19;
reconsider X1 = X, Y1 = Y as Subset of (TopSpaceNorm E) ;
A7: X1 is open by A1, NORMSP_2:16;
[#] (TopSpaceNorm E) <> {} ;
then H1 " X1 is open by A6, A7, TOPS_2:43;
then A9: H " X is open by NORMSP_2:16;
for s being object holds
( s in H " X iff s in Y )

proof

let s be object ; :: thesis: ( s in H " X iff s in Y )

hereby :: thesis: ( s in Y implies s in H " X )

assume A10: s in H " X ; :: thesis: s in Y
then A11: ( s in dom H & H . s in X ) by FUNCT_1:def 7;
reconsider s1 = s as Point of E by A10;
A12: H . s = (1 * s1) + (- v) by A3
.= s1 - v by RLVECT_1:def 8 ;
A13: H . s = H /. s by A11, PARTFUN1:def 6;
then (H /. s) + v = s1 - (v - v) by A12, RLVECT_1:29
.= s1 - (0. E) by RLVECT_1:15
.= s1 by RLVECT_1:13 ;
hence s in Y by A2, A11, A13; :: thesis: verum

end;

assume s in Y ; :: thesis: s in H " X
then consider x being Point of E such that
A14: ( s = x + v & x in X ) by A2;
reconsider s1 = s as Point of E by A14;
H . s1 = (1 * s1) + (- v) by A3
.= (x + v) - v by A14, RLVECT_1:def 8
.= x + (v - v) by RLVECT_1:28
.= x + (0. E) by RLVECT_1:15
.= x by RLVECT_1:def 4 ;
hence s in H " X by A4, A14, FUNCT_1:def 7; :: thesis: verum

end;

hence Y is open by A9, TARSKI:2; :: thesis: verum