let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds

ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) )

assume A1: OAS = OASpace V ; :: thesis: ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

consider a, b, c, d being Element of OAS such that

A2: ( not a,b // c,d & not a,b // d,c ) by ANALOAF:def 5;

reconsider u = a, v = b, w = c, y = d as VECTOR of V by A1, Th3;

take z1 = v - u; :: thesis: ex v being VECTOR of V st

for a, b being Real st (a * z1) + (b * v) = 0. V holds

( a = 0 & b = 0 )

take z2 = y - w; :: thesis: for a, b being Real st (a * z1) + (b * z2) = 0. V holds

( a = 0 & b = 0 )

( a = 0 & b = 0 ) ; :: thesis: verum

ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) )

assume A1: OAS = OASpace V ; :: thesis: ex u, v being VECTOR of V st

for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 )

consider a, b, c, d being Element of OAS such that

A2: ( not a,b // c,d & not a,b // d,c ) by ANALOAF:def 5;

reconsider u = a, v = b, w = c, y = d as VECTOR of V by A1, Th3;

take z1 = v - u; :: thesis: ex v being VECTOR of V st

for a, b being Real st (a * z1) + (b * v) = 0. V holds

( a = 0 & b = 0 )

take z2 = y - w; :: thesis: for a, b being Real st (a * z1) + (b * z2) = 0. V holds

( a = 0 & b = 0 )

now :: thesis: for r1, r2 being Real st (r1 * z1) + (r2 * z2) = 0. V & ( r1 <> 0 or r2 <> 0 ) holds

( r1 = 0 & r2 = 0 )

hence
for a, b being Real st (a * z1) + (b * z2) = 0. V holds ( r1 = 0 & r2 = 0 )

let r1, r2 be Real; :: thesis: ( (r1 * z1) + (r2 * z2) = 0. V & ( r1 <> 0 or r2 <> 0 ) implies ( r1 = 0 & r2 = 0 ) )

assume (r1 * z1) + (r2 * z2) = 0. V ; :: thesis: ( ( r1 <> 0 or r2 <> 0 ) implies ( r1 = 0 & r2 = 0 ) )

then A3: r1 * z1 = - (r2 * z2) by RLVECT_1:6

.= r2 * (- z2) by RLVECT_1:25

.= (- r2) * z2 by RLVECT_1:24 ;

assume ( r1 <> 0 or r2 <> 0 ) ; :: thesis: ( r1 = 0 & r2 = 0 )

then ( r1 <> 0 or - r2 <> 0 ) ;

then ( u,v // w,y or u,v // y,w ) by A3, ANALMETR:14;

hence ( r1 = 0 & r2 = 0 ) by A1, A2, GEOMTRAP:2; :: thesis: verum

end;assume (r1 * z1) + (r2 * z2) = 0. V ; :: thesis: ( ( r1 <> 0 or r2 <> 0 ) implies ( r1 = 0 & r2 = 0 ) )

then A3: r1 * z1 = - (r2 * z2) by RLVECT_1:6

.= r2 * (- z2) by RLVECT_1:25

.= (- r2) * z2 by RLVECT_1:24 ;

assume ( r1 <> 0 or r2 <> 0 ) ; :: thesis: ( r1 = 0 & r2 = 0 )

then ( r1 <> 0 or - r2 <> 0 ) ;

then ( u,v // w,y or u,v // y,w ) by A3, ANALMETR:14;

hence ( r1 = 0 & r2 = 0 ) by A1, A2, GEOMTRAP:2; :: thesis: verum

( a = 0 & b = 0 ) ; :: thesis: verum