let c be Element of COMPLEX ; :: thesis: ex r, s being Element of REAL st c = [*r,s*]

per cases ( c in REAL or not c in REAL ) ;

suppose c in REAL ; :: thesis: ex r, s being Element of REAL st c = [*r,s*]

then reconsider r = c, z = 0 as Element of REAL ;
take r ; :: thesis: ex s being Element of REAL st c = [*r,s*]
take z ; :: thesis: c = [*r,z*]
thus c = [*r,z*] by Def7; :: thesis: verum

end;

suppose not c in REAL ; :: thesis: 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 NUMBERS:def 2, 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:12;
0 in {0 ,1} by TARSKI:def 2;
then f . 0 in rng f by A3, FUNCT_1:12;
then reconsider r = f . 0 , s = f . 1 as Element of REAL by A4, A5;
take r ; :: thesis: ex s being Element of REAL st c = [*r,s*]
take s ; :: thesis: c = [*r,s*]
A6: c = 0 ,1 --> r,s by A2, A3, FUNCT_4:69;

now

assume s = 0 ; :: thesis: contradiction
then (0 ,1 --> r,s) . 1 = 0 by FUNCT_4:66;
then c in { x where x is Element of Funcs {0 ,1},REAL : x . 1 = 0 } by A1, A6;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

hence c = [*r,s*] by A6, Def7; :: thesis: verum

end;

end;