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

( 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

hence
D is dense
by NORMSP_3:17; :: thesis: verum
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;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