let c1, c2 be Number ; ( ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c1 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Real st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c2 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) implies c1 = c2 )
given x1, x2, x3, x4, y1, y2, y3, y4 being Real such that A3:
x = [*x1,x2,x3,x4*]
and
A4:
y = [*y1,y2,y3,y4*]
and
A5:
c1 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*]
; ( for x1, x2, x3, x4, y1, y2, y3, y4 being Real holds
( not x = [*x1,x2,x3,x4*] or not y = [*y1,y2,y3,y4*] or not c2 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) or c1 = c2 )
given x19, x29, x39, x49, y19, y29, y39, y49 being Real such that A6:
x = [*x19,x29,x39,x49*]
and
A7:
y = [*y19,y29,y39,y49*]
and
A8:
c2 = [*((((x19 * y19) - (x29 * y29)) - (x39 * y39)) - (x49 * y49)),((((x19 * y29) + (x29 * y19)) + (x39 * y49)) - (x49 * y39)),((((x19 * y39) + (y19 * x39)) + (y29 * x49)) - (y49 * x29)),((((x19 * y49) + (x49 * y19)) + (x29 * y39)) - (x39 * y29))*]
; c1 = c2
A9:
x1 = x19
by A3, A6, Th5;
A10:
x2 = x29
by A3, A6, Th5;
A11:
x3 = x39
by A3, A6, Th5;
A12:
x4 = x49
by A3, A6, Th5;
A13:
y1 = y19
by A4, A7, Th5;
A14:
y2 = y29
by A4, A7, Th5;
A15:
y3 = y39
by A4, A7, Th5;
y4 = y49
by A4, A7, Th5;
hence
c1 = c2
by A5, A8, A9, A10, A11, A12, A13, A14, A15; verum