take
doubleLoopStr(# COMPLEX,addcomplex,multcomplex,1r,0c #)
; ( 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 )
; verum