let X be RealNormSpace; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: for D being Subset of Z st D0 is dense & D0 = D holds
D is dense
let D be Subset of Z; :: thesis: ( D0 is dense & D0 = D implies D is dense )
assume A2: ( D0 is dense & D0 = D ) ; :: thesis: 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; :: thesis: ( S <> {} & S is open implies D meets S )
assume A5: ( S <> {} & S is open ) ; :: thesis: 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; :: thesis: verum

end;

hence D is dense by NORMSP_3:17; :: thesis: verum