let c be Element of COMPLEX ; ex r, s being Element of REAL st c = [*r,s*]
per cases
( c in REAL or not c in REAL )
;
suppose
not
c in REAL
;
ex r, s being Element of REAL st c = [*r,s*]then A1:
c in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 }
by XBOOLE_0:def 3;
then consider f being
Function such that A2:
c = f
and A3:
dom f = {0,1}
and A4:
rng f c= REAL
by FUNCT_2:def 2;
1
in {0,1}
by TARSKI:def 2;
then A5:
f . 1
in rng f
by A3, FUNCT_1:3;
0 in {0,1}
by TARSKI:def 2;
then
f . 0 in rng f
by A3, FUNCT_1:3;
then reconsider r =
f . 0,
s =
f . 1 as
Element of
REAL by A4, A5;
take
r
;
ex s being Element of REAL st c = [*r,s*]take
s
;
c = [*r,s*]A6:
c = (
0,1)
--> (
r,
s)
by A2, A3, FUNCT_4:66;
hence
c = [*r,s*]
by A6, Def5;
verum end; end;