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 for a, b being Real st (a * u) + (b * v) = 0. (TOP-REAL 2) holds
( a = 0 & b = 0 )let a,
b be
Real;
( (a * u) + (b * v) = 0. (TOP-REAL 2) implies ( a = 0 & b = 0 ) )assume A1:
(a * u) + (b * v) = 0. (TOP-REAL 2)
;
( 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;
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 )
;
verum
end;
hence
OASpace (TOP-REAL 2) is OAffinSpace
by ANALOAF:26; verum