let q, p be Real; :: thesis: ( q <> 0 implies ex y being Real st p = y * q )
reconsider y = p / q as Real ;
assume A1: q <> 0 ; :: thesis: ex y being Real st p = y * q
take y ; :: thesis: p = y * q
thus p = y * q by A1, XCMPLX_1:88; :: thesis: verum