thus
( z in COMPLEX implies ex IT being Number ex z9 being Complex st
( z = z9 & IT = Re z9 ) )
( not z in COMPLEX implies ex b1 being Number ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) )proof
assume
z in COMPLEX
;
ex IT being Number ex z9 being Complex st
( z = z9 & IT = Re z9 )
then consider r,
s being
Element of
REAL such that A1:
z = [*r,s*]
by ARYTM_0:9;
set z9 =
[*r,s*];
take
Re [*r,s*]
;
ex z9 being Complex st
( z = z9 & Re [*r,s*] = Re z9 )
take
[*r,s*]
;
( z = [*r,s*] & Re [*r,s*] = Re [*r,s*] )
thus
(
z = [*r,s*] &
Re [*r,s*] = Re [*r,s*] )
by A1;
verum
end;
assume A2:
not z in COMPLEX
; ex b1 being Number ex f being Function of 4,REAL st
( z = f & b1 = f . 0 )
z in QUATERNION
by Def2;
then
z in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) }
by A2, XBOOLE_0:def 3;
then reconsider f = z as Function of 4,REAL by FUNCT_2:66;
take
f . 0
; ex f being Function of 4,REAL st
( z = f & f . 0 = f . 0 )
take
f
; ( z = f & f . 0 = f . 0 )
thus
( z = f & f . 0 = f . 0 )
; verum