ex u, v being VECTOR of (TOP-REAL 2) st
for a, b being Real st (a * u) + (b * v) = 0. (TOP-REAL 2) holds
( a = 0 & b = 0 )

proof

reconsider u = |[1,0]|, v = |[0,1]| as VECTOR of (TOP-REAL 2) ;

now :: thesis: for a, b being Real st (a * u) + (b * v) = 0. (TOP-REAL 2) holds
( a = 0 & b = 0 )

let a, b be Real; :: thesis: ( (a * u) + (b * v) = 0. (TOP-REAL 2) implies ( a = 0 & b = 0 ) )
assume A1: (a * u) + (b * v) = 0. (TOP-REAL 2) ; :: thesis: ( a = 0 & b = 0 )
A2: (a * u) + (b * v) = |[(a * 1),(a * 0)]| + (b * v) by EUCLID:58
.= |[(a * 1),(a * 0)]| + |[(b * 0),(b * 1)]| by EUCLID:58
.= |[(a + 0),(0 + b)]| by EUCLID:56
.= |[a,b]| ;
( |[a,b]| `1 = a & |[a,b]| `2 = b & |[0,0]| `1 = 0 & |[0,0]| `2 = 0 ) by EUCLID:52;
hence ( a = 0 & b = 0 ) by A1, A2, EUCLID:54; :: thesis: verum

end;

hence ex u, v being VECTOR of (TOP-REAL 2) st
for a, b being Real st (a * u) + (b * v) = 0. (TOP-REAL 2) holds
( a = 0 & b = 0 ) ; :: thesis: verum

end;

hence OASpace (TOP-REAL 2) is OAffinSpace by ANALOAF:26; :: thesis: verum