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

( 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

y <> 0. V
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;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

proof

hence
( x <> 0. V & y <> 0. V )
by A2; :: thesis: verum
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;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