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 :: thesis: not (0,1) --> (0,1) in { x where x is Element of Funcs ({0,one},REAL) : x . one = 0 }
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:63; :: thesis: verum
end;
REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7;
then A2: REAL+ c= REAL by ARYTM_2:3, ZFMISC_1:34;
then reconsider z = 0 , j = 1 as Element of REAL by ARYTM_2:20;
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:20, FUNCT_4:62, ZFMISC_1:32;
then ( dom ((0,1) --> (0,1)) = {0,1} & rng ((0,1) --> (0,1)) c= REAL ) by FUNCT_4:62;
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