let X be RealLinearSpace; RLSp2RVSp ((0). X) = (0). (RLSp2RVSp X)
set Y = (0). X;
A1: the carrier of ((0). (RLSp2RVSp X)) =
{(0. (RLSp2RVSp X))}
by VECTSP_4:def 3
.=
{(0. X)}
;
A2: the addF of (RLSp2RVSp ((0). X)) =
the addF of (RLSp2RVSp X) || the carrier of (RLSp2RVSp ((0). X))
by VECTSP_4:def 2
.=
the addF of (RLSp2RVSp X) || the carrier of ((0). (RLSp2RVSp X))
by A1, RLSUB_1:def 3
.=
the addF of ((0). (RLSp2RVSp X))
by VECTSP_4:def 2
;
A3: 0. (RLSp2RVSp ((0). X)) =
0. (RLSp2RVSp X)
by VECTSP_4:def 2
.=
0. ((0). (RLSp2RVSp X))
by VECTSP_4:def 2
;
MultF_Real* ((0). X) =
the Mult of X | [:REAL, the carrier of ((0). X):]
by RLSUB_1:def 2
.=
the lmult of (RLSp2RVSp X) | [: the carrier of F_Real, the carrier of ((0). (RLSp2RVSp X)):]
by A1, RLSUB_1:def 3
.=
the lmult of ((0). (RLSp2RVSp X))
by VECTSP_4:def 2
;
hence
RLSp2RVSp ((0). X) = (0). (RLSp2RVSp X)
by A1, A2, A3, RLSUB_1:def 3; verum