let r125, r136, r246, r345, r126, r135, r245, r346, r157, r259, r597, r368, r268, r297, r247, r287, r358, r587 be non zero Real; ( ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 & r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) implies r287 * r597 = r297 * r587 )
assume that
A1:
((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346
and
A2:
r157 * r259 = - (r125 * r597)
and
A3:
r126 * r368 = r136 * r268
and
A4:
r245 * r297 = - (r247 * r259)
and
A5:
r247 * r268 = - (r246 * r287)
and
A6:
r346 * r358 = r345 * r368
and
A7:
r135 * r587 = - (r157 * r358)
; r287 * r597 = r297 * r587
reconsider r1 = ((((((((((((r246 * r125) * r247) * r259) * r136) * r268) * r345) * r368) * r157) * r358) * r126) * r135) * r245) * r346, r2 = ((((((((((((r247 * r268) * r157) * r259) * r245) * r126) * r368) * r346) * r358) * r135) * r125) * r136) * r246) * r345 as non zero Real ;
((((((- (r287 * r246)) * (- (r125 * r597))) * (- (r247 * r259))) * (r136 * r268)) * (r345 * r368)) * (- (r157 * r358))) * (((r126 * r135) * r245) * r346) = ((((((r247 * r268) * (r157 * r259)) * (r245 * r297)) * (r126 * r368)) * (r346 * r358)) * (r135 * r587)) * (((r125 * r136) * r246) * r345)
by A1, A2, A3, A4, A5, A6, A7;
then
( r1 * (r287 * r597) = r2 * (r297 * r587) & r1 <> 0 & r2 <> 0 )
by ORDINAL1:def 14;
hence
r287 * r597 = r297 * r587
by XCMPLX_1:5; verum