set X = { x where x is Element of Funcs {0 ,one },REAL : x . one = 0 } ;
thus REAL c= COMPLEX by XBOOLE_1:7; :: according to XBOOLE_0:def 8 :: thesis: not REAL = COMPLEX

A1: 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;

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