let g be Element of QUATERNION ; ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
per cases
( g in COMPLEX or not g in COMPLEX )
;
suppose
g in COMPLEX
;
ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]then consider r,
s being
Element of
REAL such that A1:
g = [*r,s*]
by ARYTM_0:11;
take
r
;
ex s, t, u being Element of REAL st g = [*r,s,t,u*]take
s
;
ex t, u being Element of REAL st g = [*r,s,t,u*]take
0
;
ex u being Element of REAL st g = [*r,s,0 ,u*]take
0
;
g = [*r,s,0 ,0 *]thus
g = [*r,s,0 ,0 *]
by A1, Def6;
verum end; suppose
not
g in COMPLEX
;
ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]then A2:
g in (Funcs 4,REAL ) \ { x where x is Element of Funcs 4,REAL : ( x . 2 = 0 & x . 3 = 0 ) }
by XBOOLE_0:def 3;
then consider f being
Function such that A3:
g = f
and A4:
dom f = 4
and A5:
rng f c= REAL
by FUNCT_2:def 2;
A6:
0 in 4
by CARD_1:90, ENUMSET1:def 2;
A7:
1
in 4
by CARD_1:90, ENUMSET1:def 2;
A8:
2
in 4
by CARD_1:90, ENUMSET1:def 2;
A9:
3
in 4
by CARD_1:90, ENUMSET1:def 2;
A10:
f . 0 in rng f
by A4, A6, FUNCT_1:12;
A11:
f . 1
in rng f
by A4, A7, FUNCT_1:12;
A12:
f . 2
in rng f
by A4, A8, FUNCT_1:12;
f . 3
in rng f
by A4, A9, FUNCT_1:12;
then reconsider r =
f . 0 ,
s =
f . 1,
t =
f . 2,
u =
f . 3 as
Element of
REAL by A5, A10, A11, A12;
A13:
g = 0 ,1,2,3
--> r,
s,
t,
u
by A3, A4, Th6, CARD_1:90;
take
r
;
ex s, t, u being Element of REAL st g = [*r,s,t,u*]take
s
;
ex t, u being Element of REAL st g = [*r,s,t,u*]take
t
;
ex u being Element of REAL st g = [*r,s,t,u*]take
u
;
g = [*r,s,t,u*]now assume that A14:
t = 0
and A15:
u = 0
;
contradictionA16:
(0 ,1,2,3 --> r,s,t,u) . 2
= 0
by A14, Lm1, Th3;
(0 ,1,2,3 --> r,s,t,u) . 3
= 0
by A15, Lm1, Th3;
then
g in { x where x is Element of Funcs 4,REAL : ( x . 2 = 0 & x . 3 = 0 ) }
by A2, A13, A16;
hence
contradiction
by A2, XBOOLE_0:def 5;
verum end; hence
g = [*r,s,t,u*]
by A13, Def6;
verum end;