let a, b, c, d be Real; ( a <> 0 & b = 0 & a * d = b * c implies ex e being Real st
( c = e * a & d = e * b ) )
assume that
A1:
a <> 0
and
A2:
b = 0
and
A3:
a * d = b * c
; ex e being Real st
( c = e * a & d = e * b )
A4:
c = (c / a) * a
by A1, XCMPLX_1:87;
(c / a) * b = d
by A1, A2, A3;
hence
ex e being Real st
( c = e * a & d = e * b )
by A4; verum