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 )
proof
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;
thus u <> 0. V :: thesis: v <> 0. V
proof
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;
thus v <> 0. V :: 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;