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 by Lm3;
take r ; :: thesis: ex s being Element of REAL st c = [*r,s*]
take z ; :: thesis: c = [*r,z*]
thus c = [*r,z*] by Def5; :: 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 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 ; :: 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:66;

now :: thesis: not s = 0

assume s = 0 ; :: thesis: contradiction
then ((0,1) --> (r,s)) . 1 = 0 by FUNCT_4:63;
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, Def5; :: thesis: verum

end;

end;