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 )

per cases ( a <> 0 or a = 0 ) ;

suppose A3: a <> 0 ; :: thesis: ex e being Real st
( c = e * a & d = e * b )

per cases ( b = 0 or b <> 0 ) ;

suppose b = 0 ; :: thesis: ex e being Real st
( c = e * a & d = e * b )

hence ex e being Real st
( c = e * a & d = e * b ) by A1, A2, Lem02; :: thesis: verum

end;

suppose b <> 0 ; :: 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 ) by A2, A3, Lem01;
hence ex e being Real st
( c = e * a & d = e * b ) ; :: thesis: verum

end;

end;

end;

suppose a = 0 ; :: thesis: ex e being Real st
( c = e * a & d = e * b )

then ex e being Real st
( d = e * b & c = e * a ) by A1, A2, Lem02;
hence ex e being Real st
( c = e * a & d = e * b ) ; :: thesis: verum

end;

end;