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