let c1, c2 be Number ; ( 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))*]
; ( 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))*]
; 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; verum