:: deftheorem Def5 defines [* QUATERNI:def 5 :
for x, y, w, z being Real
for b₅ being Element of QUATERNION holds
( ( w = 0 & z = 0 implies ( b₅ = [*x,y,w,z*] iff ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b₅ = [*x9,y9*] ) ) ) & ( ( not w = 0 or not z = 0 ) implies ( b₅ = [*x,y,w,z*] iff b₅ = (0,1,2,3) --> (x,y,w,z) ) ) );