theorem Th64: :: COMPLSP2:75

for x, y being FinSequence of COMPLEX holds |(x,y)| = |(y,x)| *'