theorem :: QUATERNI:69

|.<i>.| = 1 by Th23, SQUARE_1:18;