( 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) & 0.REAL 2 = |[0,0]| ) by Def8, FINSEQ_2:61;
hence 0. (TOP-REAL 2) = |[0,0]| ; :: thesis: verum