:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :
for b₁ being strict doubleLoopStr holds
( b₁ = F_Complex iff ( the carrier of b₁ = COMPLEX & the addF of b₁ = addcomplex & the multF of b₁ = multcomplex & 1. b₁ = 1r & 0. b₁ = 0c ) );