let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
( x <> 0. V & y <> 0. V )
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies ( x <> 0. V & y <> 0. V ) )
assume A1: Gen x,y ; :: thesis: ( x <> 0. V & y <> 0. V )
A2: x <> 0. V
proof
assume A3: x = 0. V ; :: thesis: contradiction
consider a, b being Real such that
A4: a = 1 and
A5: b = 0 ;
(a * x) + (b * y) = (0. V) + (0 * y) by A3, A5, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A1, A4, ANALMETR:def 1; :: thesis: verum
end;
y <> 0. V
proof
assume A6: y = 0. V ; :: thesis: contradiction
consider a, b being Real such that
A7: a = 0 and
A8: b = 1 ;
(a * x) + (b * y) = (0. V) + (1 * (0. V)) by A6, A7, A8, RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A1, A8, ANALMETR:def 1; :: thesis: verum
end;
hence ( x <> 0. V & y <> 0. V ) by A2; :: thesis: verum