let g be Quaternion; ex r, s, t, u being Real st g = [*r,s,t,u*]
A1:
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 Real st g = [*r,s,t,u*]then consider r,
s being
Element of
REAL such that A2:
g = [*r,s*]
by ARYTM_0:9;
take
r
;
ex s, t, u being Real st g = [*r,s,t,u*]take
s
;
ex t, u being Real st g = [*r,s,t,u*]take
0
;
ex u being Real st g = [*r,s,0,u*]take
0
;
g = [*r,s,0,0*]thus
g = [*r,s,0,0*]
by A2, Def5, A1;
verum end; suppose
not
g in COMPLEX
;
ex r, s, t, u being Real st g = [*r,s,t,u*]then A3:
g in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) }
by A1, XBOOLE_0:def 3;
then consider f being
Function such that A4:
g = f
and A5:
dom f = 4
and A6:
rng f c= REAL
by FUNCT_2:def 2;
A7:
0 in 4
by CARD_1:52, ENUMSET1:def 2;
A8:
1
in 4
by CARD_1:52, ENUMSET1:def 2;
A9:
2
in 4
by CARD_1:52, ENUMSET1:def 2;
A10:
3
in 4
by CARD_1:52, ENUMSET1:def 2;
A11:
f . 0 in rng f
by A5, A7, FUNCT_1:3;
A12:
f . 1
in rng f
by A5, A8, FUNCT_1:3;
A13:
f . 2
in rng f
by A5, A9, FUNCT_1:3;
f . 3
in rng f
by A5, A10, FUNCT_1:3;
then reconsider r =
f . 0,
s =
f . 1,
t =
f . 2,
u =
f . 3 as
Element of
REAL by A6, A11, A12, A13;
A14:
g = (
0,1,2,3)
--> (
r,
s,
t,
u)
by A4, A5, FUNCT_4:144, CARD_1:52;
take
r
;
ex s, t, u being Real st g = [*r,s,t,u*]take
s
;
ex t, u being Real st g = [*r,s,t,u*]take
t
;
ex u being Real st g = [*r,s,t,u*]take
u
;
g = [*r,s,t,u*]now ( t = 0 implies not u = 0 )assume that A15:
t = 0
and A16:
u = 0
;
contradictionA17:
((0,1,2,3) --> (r,s,t,u)) . 2
= 0
by A15, FUNCT_4:140;
((0,1,2,3) --> (r,s,t,u)) . 3
= 0
by A16, FUNCT_4:139;
then
g in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) }
by A3, A14, A17;
hence
contradiction
by A3, XBOOLE_0:def 5;
verum end; hence
g = [*r,s,t,u*]
by A14, Def5;
verum end;