let V be RealLinearSpace; for W being Subspace of V holds (0). W = (0). V
let W be Subspace of V; (0). W = (0). V
( the carrier of ((0). W) = {(0. W)} & the carrier of ((0). V) = {(0. V)} )
by Def3;
then A1:
the carrier of ((0). W) = the carrier of ((0). V)
by Def2;
(0). W is Subspace of V
by Th27;
hence
(0). W = (0). V
by A1, Th30; verum