:: deftheorem defines |( COMPLSP2:def 4 :
for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;