let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies ( w <> 0. V & y <> 0. V ) )
assume A1: Gen w,y ; :: thesis: ( w <> 0. V & y <> 0. V )
thus w <> 0. V :: thesis: y <> 0. V

proof

assume w = 0. V ; :: thesis: contradiction
then 0. V = 1 * w by RLVECT_1:def 8
.= (1 * w) + (0. V) by RLVECT_1:4
.= (1 * w) + (0 * y) by RLVECT_1:10 ;
hence contradiction by A1; :: thesis: verum

end;

thus y <> 0. V :: thesis: verum

proof

assume y = 0. V ; :: thesis: contradiction
then 0. V = 1 * y by RLVECT_1:def 8
.= (0. V) + (1 * y) by RLVECT_1:4
.= (0 * w) + (1 * y) by RLVECT_1:10 ;
hence contradiction by A1; :: thesis: verum

end;