let a2, c2, a3, c3 be Real; :: thesis: for A1, A19, B1, B19 being Real st A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 & B1 * c3 = B19 * c2 & a2 <> a3 & c2 <> 0 holds
A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1
let A1, A19, B1, B19 be Real; :: thesis: ( A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 & B1 * c3 = B19 * c2 & a2 <> a3 & c2 <> 0 implies A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 )
assume that
A1: A1 + B1 = A19 + B19 and
A2: ( A1 * a2 = A19 * a3 & B1 * c3 = B19 * c2 ) and
A3: ( a2 <> a3 & c2 <> 0 ) ; :: thesis: A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1
A4: (A1 * (a3 * c2)) + (B1 * (a3 * c2)) = (A19 + B19) * (a3 * c2) by A1, XCMPLX_1:8;
( A1 * (a2 * c2) = (A19 * a3) * c2 & B1 * (c3 * a3) = (B19 * c2) * a3 ) by A2, XCMPLX_1:4;
then B1 * ((a3 * c3) - (a3 * c2)) = A1 * ((a3 * c2) - (a2 * c2)) by A4;
then A5: A1 * (((a3 * c2) - (a2 * c2)) * (((a3 * c2) - (a2 * c2)) ")) = (B1 * ((a3 * c3) - (a3 * c2))) * (((a3 * c2) - (a2 * c2)) ") by XCMPLX_1:4;
(a3 * c2) - (a2 * c2) <> 0 by A3, Lm23;
then A1 * 1 = (B1 * ((a3 * c3) - (a3 * c2))) * (((a3 * c2) - (a2 * c2)) ") by A5, XCMPLX_0:def 7;
hence A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 ; :: thesis: verum