reconsider x9 = x, y9 = y, w9 = w, z9 = z as Element of REAL by XREAL_0:def 1;
thus ( w = 0 & z = 0 implies ex t being Element of QUATERNION ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] ) ) :: 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 x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
set t = [*x9,y9*];
reconsider t = [*x9,y9*] as Element of QUATERNION by XBOOLE_0:def 3;
take t ; :: thesis: ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
take x9 ; :: thesis: ex y9 being Element of REAL st
( x9 = x & y9 = y & t = [*x9,y9*] )
take y9 ; :: thesis: ( x9 = x & y9 = y & t = [*x9,y9*] )
thus ( x9 = x & y9 = y & t = [*x9,y9*] ) ; :: thesis: verum

end;

set e = 0 ,1,2,3 --> x9,y9,w9,z9;
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 --> x9,y9,w9,z9 in Funcs 4,REAL by CARD_1:90, FUNCT_2:11;

now

assume 0 ,1,2,3 --> x9,y9,w9,z9 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 --> x9,y9,w9,z9 = r & r . 2 = 0 & r . 3 = 0 ) ;
hence contradiction by A1, Lm1, Th3; :: thesis: verum

end;

then 0 ,1,2,3 --> x9,y9,w9,z9 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 --> x9,y9,w9,z9 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