theorem Th25: :: QUATERN2:25

for x1, x2, x3, x4 being Real holds [*x1,x2,x3,x4*] *' = [*x1,(- x2),(- x3),(- x4)*]