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 q09, q19, q29, q39, r09, r19, r29, r39 being Element of REAL such that A6: q = [*q09,q19,q29,q39*] and
A7: r = [*r09,r19,r29,r39*] and
A8: c2 = [*(((((r09 * q09) + (r19 * q19)) + (r29 * q29)) + (r39 * q39)) / (|.r.| ^2)),(((((r09 * q19) - (r19 * q09)) - (r29 * q39)) + (r39 * q29)) / (|.r.| ^2)),(((((r09 * q29) + (r19 * q39)) - (r29 * q09)) - (r39 * q19)) / (|.r.| ^2)),(((((r09 * q39) - (r19 * q29)) + (r29 * q19)) - (r39 * q09)) / (|.r.| ^2))*] ; :: thesis: c1 = c2
A9: q0 = q09 by A3, A6, QUATERNI:12;
A10: q1 = q19 by A3, A6, QUATERNI:12;
A11: q2 = q29 by A3, A6, QUATERNI:12;
A12: q3 = q39 by A3, A6, QUATERNI:12;
A13: r0 = r09 by A4, A7, QUATERNI:12;
A14: r1 = r19 by A4, A7, QUATERNI:12;
A15: r2 = r29 by A4, A7, QUATERNI:12;
r3 = r39 by A4, A7, QUATERNI:12;
hence c1 = c2 by A5, A8, A9, A10, A11, A12, A13, A14, A15; :: thesis: verum