let p be Element of V; :: thesis: ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 )
1 * p = 1 * p ;
hence ex a, b being Real st
( a * p = b * p & a <> 0 & b <> 0 ) ; :: thesis: verum