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 )
now :: thesis: for r1, r2 being Real st (r1 * z1) + (r2 * z2) = 0. V & ( r1 <> 0 or r2 <> 0 ) 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;
hence for a, b being Real st (a * z1) + (b * z2) = 0. V holds
( a = 0 & b = 0 ) ; :: thesis: verum