let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V st ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) holds

( u <> v & u <> 0. V & v <> 0. V )

let u, v be VECTOR of V; :: thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) implies ( u <> v & u <> 0. V & v <> 0. V ) )

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

( a = 0 & b = 0 ) ; :: thesis: ( u <> v & u <> 0. V & v <> 0. V )

thus u <> v :: thesis: ( u <> 0. V & v <> 0. V )

( a = 0 & b = 0 ) ) holds

( u <> v & u <> 0. V & v <> 0. V )

let u, v be VECTOR of V; :: thesis: ( ( for a, b being Real st (a * u) + (b * v) = 0. V holds

( a = 0 & b = 0 ) ) implies ( u <> v & u <> 0. V & v <> 0. V ) )

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

( a = 0 & b = 0 ) ; :: thesis: ( u <> v & u <> 0. V & v <> 0. V )

thus u <> v :: thesis: ( u <> 0. V & v <> 0. V )

proof

thus
u <> 0. V
:: thesis: v <> 0. V
assume
u = v
; :: thesis: contradiction

then u - v = 0. V by RLVECT_1:15;

then (1 * u) + (- v) = 0. V by RLVECT_1:def 8;

then (1 * u) + ((- jj) * v) = 0. V by RLVECT_1:16;

hence contradiction by A1; :: thesis: verum

end;then u - v = 0. V by RLVECT_1:15;

then (1 * u) + (- v) = 0. V by RLVECT_1:def 8;

then (1 * u) + ((- jj) * v) = 0. V by RLVECT_1:16;

hence contradiction by A1; :: thesis: verum

proof

thus
v <> 0. V
:: thesis: verum
assume
u = 0. V
; :: thesis: contradiction

then 1 * u = 0. V by RLVECT_1:10;

then (1 * u) + (0. V) = 0. V by RLVECT_1:4;

then (jj * u) + (0 * v) = 0. V by RLVECT_1:10;

hence contradiction by A1; :: thesis: verum

end;then 1 * u = 0. V by RLVECT_1:10;

then (1 * u) + (0. V) = 0. V by RLVECT_1:4;

then (jj * u) + (0 * v) = 0. V by RLVECT_1:10;

hence contradiction by A1; :: thesis: verum

proof

assume
v = 0. V
; :: thesis: contradiction

then 1 * v = 0. V by RLVECT_1:10;

then (0. V) + (1 * v) = 0. V by RLVECT_1:4;

then (0 * u) + (jj * v) = 0. V by RLVECT_1:10;

hence contradiction by A1; :: thesis: verum

end;then 1 * v = 0. V by RLVECT_1:10;

then (0. V) + (1 * v) = 0. V by RLVECT_1:4;

then (0 * u) + (jj * v) = 0. V by RLVECT_1:10;

hence contradiction by A1; :: thesis: verum