reconsider x' = x, y' = y, w' = w, z' = z as Element of REAL by XREAL_0:def 1;
thus ( w = 0 & z = 0 implies ex t being Element of QUATERNION ex x', y' being Element of REAL st
( x' = x & y' = y & t = [*x',y'*] ) ) :: thesis: ( ( not w = 0 or not z = 0 ) implies ex b₁ being Element of QUATERNION st b₁ = 0 ,1,2,3 --> x,y,w,z )

proof

assume that
w = 0 and
z = 0 ; :: thesis: ex t being Element of QUATERNION ex x', y' being Element of REAL st
( x' = x & y' = y & t = [*x',y'*] )
set t = [*x',y'*];
reconsider t = [*x',y'*] as Element of QUATERNION by XBOOLE_0:def 3;
take t ; :: thesis: ex x', y' being Element of REAL st
( x' = x & y' = y & t = [*x',y'*] )
take x' ; :: thesis: ex y' being Element of REAL st
( x' = x & y' = y & t = [*x',y'*] )
take y' ; :: thesis: ( x' = x & y' = y & t = [*x',y'*] )
thus ( x' = x & y' = y & t = [*x',y'*] ) ; :: thesis: verum

end;

set e = 0 ,1,2,3 --> x',y',w',z';
thus ( ( w <> 0 or z <> 0 ) implies ex t being Element of QUATERNION st t = 0 ,1,2,3 --> x,y,w,z ) :: thesis: verum

proof

assume A1: ( w <> 0 or z <> 0 ) ; :: thesis: ex t being Element of QUATERNION st t = 0 ,1,2,3 --> x,y,w,z
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;
then reconsider e = 0 ,1,2,3 --> x',y',w',z' as Element of QUATERNION by XBOOLE_0:def 3;
take e ; :: thesis: e = 0 ,1,2,3 --> x,y,w,z
thus e = 0 ,1,2,3 --> x,y,w,z ; :: thesis: verum

end;

thus verum ; :: thesis: verum