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