thus ( w = 0 & z = 0 implies [*x,y*] is Element of QUATERNION ) by XBOOLE_0:def 3; :: thesis: ( ( not w = 0 or not z = 0 ) implies 0 ,1,2,3 --> x,y,w,z is Element of QUATERNION )
set e = 0 ,1,2,3 --> x,y,w,z;
assume A1: ( w <> 0 or z <> 0 ) ; :: thesis: 0 ,1,2,3 --> x,y,w,z is Element of QUATERNION
A2: 0 ,1,2,3 --> x,y,w,z in Funcs 4,REAL by CARD_1:90, FUNCT_2:11;

now

assume 0 ,1,2,3 --> x,y,w,z in { r where r is Element of Funcs 4,REAL : ( r . 2 = 0 & r . 3 = 0 ) } ; :: thesis: contradiction
then ex r being Element of Funcs 4,REAL st
( 0 ,1,2,3 --> x,y,w,z = r & r . 2 = 0 & r . 3 = 0 ) ;
hence contradiction by A1, Lm1, Th3; :: thesis: verum

end;

then 0 ,1,2,3 --> x,y,w,z in (Funcs 4,REAL ) \ { r where r is Element of Funcs 4,REAL : ( r . 2 = 0 & r . 3 = 0 ) } by A2, XBOOLE_0:def 5;
hence 0 ,1,2,3 --> x,y,w,z is Element of QUATERNION by XBOOLE_0:def 3; :: thesis: verum