A: RLSStruct(# the carrier of (TOP-REAL 2),the ZeroF of (TOP-REAL 2),the addF of (TOP-REAL 2),the Mult of (TOP-REAL 2) #) = RealVectSpace (Seg 2) by Def8;
0.REAL 2 = |[0 ,0 ]| by FINSEQ_2:75;
hence 0. (TOP-REAL 2) = |[0 ,0 ]| by A; :: thesis: verum