take doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) ; :: thesis: ( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = COMPLEX & the addF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = addcomplex & the multF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = multcomplex & 1. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 1r & 0. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 0c )
thus ( the carrier of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = COMPLEX & the addF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = addcomplex & the multF of doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = multcomplex & 1. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 1r & 0. doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #) = 0c ) ; :: thesis: verum