let X be RealNormSpace; for Y, Z being SubRealNormSpace of X st ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) holds
for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense
let Y, Z be SubRealNormSpace of X; ( ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) implies for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense )
given A being Subset of X such that A1:
( A = the carrier of Y & Cl A = the carrier of Z )
; for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense
let D0 be Subset of Y; for D being Subset of Z st D0 is dense & D0 = D holds
D is dense
let D be Subset of Z; ( D0 is dense & D0 = D implies D is dense )
assume A2:
( D0 is dense & D0 = D )
; D is dense
A3:
( the carrier of (LinearTopSpaceNorm Z) = the carrier of Z & the carrier of (LinearTopSpaceNorm Y) = the carrier of Y & the carrier of (LinearTopSpaceNorm X) = the carrier of X )
by NORMSP_2:def 4;
A4:
( LinearTopSpaceNorm Z is SubSpace of LinearTopSpaceNorm X & LinearTopSpaceNorm Y is SubSpace of LinearTopSpaceNorm X )
by Th2;
for S being Subset of Z st S <> {} & S is open holds
D meets S
proof
let S be
Subset of
Z;
( S <> {} & S is open implies D meets S )
assume A5:
(
S <> {} &
S is
open )
;
D meets S
reconsider SZL =
S as
Subset of
(LinearTopSpaceNorm Z) by NORMSP_2:def 4;
reconsider SZT =
SZL as
Subset of
(TopSpaceNorm Z) ;
SZT is
open
by A5, NORMSP_2:16;
then
SZL is
open
by NORMSP_2:20;
then consider SXL being
Subset of
(LinearTopSpaceNorm X) such that A6:
(
SXL in the
topology of
(LinearTopSpaceNorm X) &
SZL = SXL /\ ([#] (LinearTopSpaceNorm Z)) )
by A4, PRE_TOPC:def 4;
reconsider SYL =
SXL /\ ([#] (LinearTopSpaceNorm Y)) as
Subset of
(LinearTopSpaceNorm Y) ;
reconsider SX =
SXL as
Subset of
X by NORMSP_2:def 4;
reconsider SXT =
SXL as
Subset of
(TopSpaceNorm X) by NORMSP_2:def 4;
reconsider SY =
SYL as
Subset of
Y by NORMSP_2:def 4;
reconsider SYT =
SYL as
Subset of
(TopSpaceNorm Y) by NORMSP_2:def 4;
SXL is
open
by A6;
then
SXT is
open
by NORMSP_2:20;
then A7:
SX is
open
by NORMSP_2:16;
SX /\ (Cl A) <> {}
by A1, A5, A6, NORMSP_2:def 4;
then consider v being
object such that A8:
v in SX /\ (Cl A)
by XBOOLE_0:def 1;
(
v in SX &
v in Cl A )
by A8, XBOOLE_0:def 4;
then
SX meets A
by A7, NORMSP_3:5;
then A9:
SYL <> {}
by A1, NORMSP_2:def 4;
SYL is
open
by A4, A6, PRE_TOPC:def 4;
then
SYT is
open
by NORMSP_2:20;
then
SY is
open
by NORMSP_2:16;
then A10:
D0 meets SY
by A2, A9, NORMSP_3:17;
SYL c= SZL
by A1, A3, A6, NORMSP_3:4, XBOOLE_1:26;
then
D /\ SYL c= D /\ SZL
by XBOOLE_1:26;
hence
D meets S
by A2, A10;
verum
end;
hence
D is dense
by NORMSP_3:17; verum