let c1, c2 be number ; :: thesis: ( ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & c1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) & ex q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL st
( q = [*q0,q1,q2,q3*] & r = [*r0,r1,r2,r3*] & c2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) implies c1 = c2 )
given q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL such that A3: q = [*q0,q1,q2,q3*] and
A4: r = [*r0,r1,r2,r3*] and
A5: c1 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ; :: thesis: ( for q0, q1, q2, q3, r0, r1, r2, r3 being Element of REAL holds
( not q = [*q0,q1,q2,q3*] or not r = [*r0,r1,r2,r3*] or not c2 = [*(((((r0 * q0) + (r1 * q1)) + (r2 * q2)) + (r3 * q3)) / (|.r.| ^2 )),(((((r0 * q1) - (r1 * q0)) - (r2 * q3)) + (r3 * q2)) / (|.r.| ^2 )),(((((r0 * q2) + (r1 * q3)) - (r2 * q0)) - (r3 * q1)) / (|.r.| ^2 )),(((((r0 * q3) - (r1 * q2)) + (r2 * q1)) - (r3 * q0)) / (|.r.| ^2 ))*] ) or c1 = c2 )
given q0', q1', q2', q3', r0', r1', r2', r3' being Element of REAL such that A6: q = [*q0',q1',q2',q3'*] and
A7: r = [*r0',r1',r2',r3'*] and
A8: c2 = [*(((((r0' * q0') + (r1' * q1')) + (r2' * q2')) + (r3' * q3')) / (|.r.| ^2 )),(((((r0' * q1') - (r1' * q0')) - (r2' * q3')) + (r3' * q2')) / (|.r.| ^2 )),(((((r0' * q2') + (r1' * q3')) - (r2' * q0')) - (r3' * q1')) / (|.r.| ^2 )),(((((r0' * q3') - (r1' * q2')) + (r2' * q1')) - (r3' * q0')) / (|.r.| ^2 ))*] ; :: thesis: c1 = c2
A9: q0 = q0' by A3, A6, QUATERNI:12;
A10: q1 = q1' by A3, A6, QUATERNI:12;
A11: q2 = q2' by A3, A6, QUATERNI:12;
A12: q3 = q3' by A3, A6, QUATERNI:12;
A13: r0 = r0' by A4, A7, QUATERNI:12;
A14: r1 = r1' by A4, A7, QUATERNI:12;
A15: r2 = r2' by A4, A7, QUATERNI:12;
r3 = r3' by A4, A7, QUATERNI:12;
hence c1 = c2 by A5, A8, A9, A10, A11, A12, A13, A14, A15; :: thesis: verum