let a, b, c, d be Real; :: thesis: ( ( a <>0 or b <>0 ) & a * d = b * c implies ex e being Real st ( c = e * a & d = e * b ) ) assume that A1:
( a <>0 or b <>0 )
and A2:
a * d = b * c
; :: thesis: ex e being Real st ( c = e * a & d = e * b )
then
ex e being Real st ( e = d / b & e = c / a & c = e * a & d = e * b )
byA2, A3, Lem01; hence
ex e being Real st ( c = e * a & d = e * b )
; :: thesis: verum