let X be RealLinearSpace; :: thesis: for Y1, Y2 being Subspace of X holds RLSp2RVSp (Y1 /\ Y2) = (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2)
let Y1, Y2 be Subspace of X; :: thesis: RLSp2RVSp (Y1 /\ Y2) = (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2)
set Y12 = Y1 /\ Y2;
the carrier of (Y1 /\ Y2) = the carrier of Y1 /\ the carrier of Y2 by RLSUB_2:def 2;
hence RLSp2RVSp (Y1 /\ Y2) = (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2) by VECTSP_5:def 2; :: thesis: verum