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