let n be Nat; :: thesis: 0. (RealVectSpace (Seg n)) = 0. (TOP-REAL n)
RealVectSpace (Seg n) = RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def 6;
hence 0. (RealVectSpace (Seg n)) = (Seg n) --> 0 by FUNCSDOM:def 4
.= 0* n by FINSEQ_2:def 2
.= 0. (TOP-REAL n) by EUCLID:70 ;
:: thesis: verum