let c1, c2 be number ; :: thesis: ( ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Element of 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 Element of 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))*] ; :: thesis: ( for x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 x1', x2', x3', x4', y1', y2', y3', y4' being Element of REAL such that A6: x = [*x1',x2',x3',x4'*] and
A7: y = [*y1',y2',y3',y4'*] and
A8: 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'))*] ; :: thesis: c1 = c2
A9: x1 = x1' by A3, A6, Th12;
A10: x2 = x2' by A3, A6, Th12;
A11: x3 = x3' by A3, A6, Th12;
A12: x4 = x4' by A3, A6, Th12;
A13: y1 = y1' by A4, A7, Th12;
A14: y2 = y2' by A4, A7, Th12;
A15: y3 = y3' by A4, A7, Th12;
y4 = y4' by A4, A7, Th12;
hence c1 = c2 by A5, A8, A9, A10, A11, A12, A13, A14, A15; :: thesis: verum