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