let x1, y1 be Element of F_Complex; :: thesis: for x2, y2 being Complex st x1 = x2 & y1 = y2 & y1 <> 0. F_Complex holds
x1 / y1 = x2 / y2
let x2, y2 be Complex; :: thesis: ( x1 = x2 & y1 = y2 & y1 <> 0. F_Complex implies x1 / y1 = x2 / y2 )
assume that
A1: x1 = x2 and
A2: y1 = y2 ; :: thesis: ( not y1 <> 0. F_Complex or x1 / y1 = x2 / y2 )
assume y1 <> 0. F_Complex ; :: thesis: x1 / y1 = x2 / y2
then y1 " = y2 " by A2, Th5;
hence x1 / y1 = x2 / y2 by A1, XCMPLX_0:def 9; :: thesis: verum