let c be Element of ; :: thesis: c is quaternion
c in the carrier of R_Quaternion ;
then c in QUATERNION by Def10;
hence c is quaternion ; :: thesis: verum