theorem Th64: :: NUMBER15:64

for c1, c2 being Complex holds <*c1,c2*> " = <*(c1 "),(c2 ")*>