let r416, r415, r413, r418, r419, r412, r712, r746, r716, r742, r715, r743, r713, r745, r749, r718, r719, r748 be non zero Real; :: thesis: ( (- r412) * (- r713) = (- r413) * (- r712) & (- r415) * (- r719) = (- r419) * (- r715) & (- r418) * (- r716) = (- r416) * (- r718) & (- r745) * r416 = (- r746) * r415 & (- r748) * r413 = (- r743) * r418 & (- r742) * r419 = (- r749) * r412 & r712 * r746 = r716 * r742 & r715 * r743 = r713 * r745 implies r718 * r749 = r719 * r748 )
assume A1: ( (- r412) * (- r713) = (- r413) * (- r712) & (- r415) * (- r719) = (- r419) * (- r715) & (- r418) * (- r716) = (- r416) * (- r718) & (- r745) * r416 = (- r746) * r415 & (- r748) * r413 = (- r743) * r418 & (- r742) * r419 = (- r749) * r412 & r712 * r746 = r716 * r742 & r715 * r743 = r713 * r745 ) ; :: thesis: r718 * r749 = r719 * r748
reconsider r146 = - r416, r145 = - r415, r143 = - r413, r148 = - r418, r149 = - r419, r142 = - r412, r172 = - r712, r476 = - r746, r176 = - r716, r472 = - r742, r175 = - r715, r473 = - r743, r173 = - r713, r475 = - r745, r478 = - r748, r479 = - r749, r178 = - r718, r179 = - r719 as non zero Real ;
A2: (((((((r142 * r173) * (r145 * r179)) * (r148 * r176)) * (r475 * r416)) * (r478 * r413)) * (r472 * r419)) * (r712 * r746)) * (r715 * r743) = (((((((r143 * r172) * (r149 * r175)) * (r146 * r178)) * (r476 * r415)) * (r473 * r418)) * (r479 * r412)) * (r716 * r742)) * (r713 * r745) by A1;
reconsider r1 = (((((((r142 * r173) * r145) * (r148 * r176)) * (r475 * r416)) * r413) * (r472 * r419)) * (r712 * r746)) * (r715 * r743), r2 = (((((((r143 * r172) * (r149 * r175)) * r146) * (r476 * r415)) * (r473 * r418)) * r412) * (r716 * r742)) * (r713 * r745) as non zero Real ;
A3: (r179 * r478) * r1 = (r178 * r479) * r1 by A2;
r1 <> 0 by ORDINAL1:def 14;
hence r718 * r749 = r719 * r748 by A3, XCMPLX_1:5; :: thesis: verum