let g be quaternion number ; ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
A:
g in QUATERNION
by Def2;
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, A;
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, A;
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;