let n be Nat; :: thesis: 0. (n -VectSp_over F_Real) = 0. (TOP-REAL n)
thus 0. (n -VectSp_over F_Real) = n |-> (0. F_Real) by MATRIX13:102
.= 0* n
.= 0. (TOP-REAL n) by EUCLID:70 ; :: thesis: verum