let V be RealLinearSpace; for v1, v2 being VECTOR of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
let v1, v2 be VECTOR of V; ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
thus
( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) )
( ( for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A6:
for a, b being Real st (a * v1) + (b * v2) = 0. V holds
( a = 0 & b = 0 )
; ( v1 <> v2 & {v1,v2} is linearly-independent )
A7:
now for a being Real holds not v1 = a * v2end;
hence
( v1 <> v2 & {v1,v2} is linearly-independent )
by A7, Th12; verum