take doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) ; :: thesis: ( the carrier of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = QUATERNION & the addF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = addquaternion & the multF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = multquaternion & 1. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 1q & 0. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 0q )
thus ( the carrier of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = QUATERNION & the addF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = addquaternion & the multF of doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = multquaternion & 1. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 1q & 0. doubleLoopStr(# QUATERNION,addquaternion,multquaternion,1q,0q #) = 0q ) ; :: thesis: verum