thus REAL c= COMPLEX by XBOOLE_1:7; :: according to XBOOLE_0:def 8 :: thesis: not REAL = COMPLEX
A1: dom (0 ,1 --> 0 ,1) = {0 ,1} by FUNCT_4:65;
A2: rng (0 ,1 --> 0 ,1) c= {0 ,1} by FUNCT_4:65;
REAL+ c= REAL+ \/ [:{{} },REAL+ :] by XBOOLE_1:7;
then A3: REAL+ c= REAL by ARYTM_2:3, ZFMISC_1:40;
then {0 ,1} c= REAL by ARYTM_2:21, ZFMISC_1:38;
then rng (0 ,1 --> 0 ,1) c= REAL by A2, XBOOLE_1:1;
then A4: 0 ,1 --> 0 ,1 in Funcs {0 ,one },REAL by A1, FUNCT_2:def 2;
reconsider z = 0 , j = 1 as Element of REAL by A3, ARYTM_2:21;
A5: not 0 ,1 --> z,j in REAL by Lm7;
set X = { x where x is Element of Funcs {0 ,one },REAL : x . one = 0 } ;

now

assume 0 ,1 --> 0 ,1 in { x where x is Element of Funcs {0 ,one },REAL : x . one = 0 } ; :: thesis: contradiction
then ex x being Element of Funcs {0 ,one },REAL st
( x = 0 ,1 --> 0 ,1 & x . one = 0 ) ;
hence contradiction by FUNCT_4:66; :: thesis: verum

end;

then 0 ,1 --> 0 ,1 in (Funcs {0 ,one },REAL ) \ { x where x is Element of Funcs {0 ,one },REAL : x . one = 0 } by A4, XBOOLE_0:def 5;
hence not REAL = COMPLEX by A5, XBOOLE_0:def 3; :: thesis: verum