K-Loops in The Minkowski World Over an Ordered Field

Let K be a commutative ordered field and L =K(i) the quadratic extension of K with i² = ?1. Let H be the set of all Hermitian 2 × 2 matrices over the field extension (L,K) and let H^(2),+ ? {A ∈ H ¦ det A ∈ K⁽²⁾, Tr A > 0}. Then we prove that (H⁽²⁾,+,⊕) is a K-loop with respect to the operation $$ {\rm A}\ \oplus \ {\rm B}= {1 \over {\rm TrA} + 2{\sqrt {\rm det A}}} ({\sqrt {\rm det A}}\ E +A){\rm B} ({\sqrt {\rm det A}}\ E +A) $$ where E is the identity matrix.