theorem Th15: :: NUMBER17:15
for c1, c2, c3, c4 being Complex holds <*c1,c2,c3,c4*> " = <*(c1 "),(c2 "),(c3 "),(c4 ")*>