theorem Th17: :: QUATERNI:24

for z being Quaternion holds z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]