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 b1 being Element of QUATERNION st b1 = (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:52, FUNCT_2:8;
now :: thesis: not (0,1,2,3) --> (x9,y9,w9,z9) in { r where r is Element of Funcs (4,REAL) : ( r . 2 = 0 & r . 3 = 0 ) }
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, FUNCT_4:139, FUNCT_4:140; :: 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;