theorem Th2: :: QUATERNI:7

for g being Quaternion ex r, s, t, u being Real st g = [*r,s,t,u*]