let V be RealUnitarySpace; for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Subspace of V; ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
0. V in W
by RUSUB_1:11;
then
0. V in the carrier of W
by STRUCT_0:def 5;
then
{(0. V)} c= the carrier of W
by ZFMISC_1:31;
then A1:
{(0. V)} /\ the carrier of W = {(0. V)}
by XBOOLE_1:28;
the carrier of (((0). V) /\ W) =
the carrier of ((0). V) /\ the carrier of W
by Def2
.=
{(0. V)} /\ the carrier of W
by RUSUB_1:def 2
;
hence
((0). V) /\ W = (0). V
by A1, RUSUB_1:def 2; W /\ ((0). V) = (0). V
hence
W /\ ((0). V) = (0). V
by Th14; verum