let x1 be set ; :: thesis: for A being non empty set st x1 in A holds
( (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL) )
let A be non empty set ; :: thesis: ( x1 in A implies ( (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL) ) )
assume a0: x1 in A ; :: thesis: ( (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL) )
A2: dom ((RealFuncZero A) +* (x1 .--> 1)) = (dom (RealFuncZero A)) \/ (dom (x1 .--> 1)) by FUNCT_4:def 1
.= (dom (RealFuncZero A)) \/ {x1}
.= A \/ {x1}
.= A by a0, XBOOLE_1:12, ZFMISC_1:31 ;
a2: dom ((RealFuncUnit A) +* (x1 .--> 0)) = (dom (RealFuncUnit A)) \/ (dom (x1 .--> 0)) by FUNCT_4:def 1
.= (dom (RealFuncUnit A)) \/ {x1}
.= A \/ {x1}
.= A by a0, XBOOLE_1:12, ZFMISC_1:31 ;
H2: rng ((RealFuncZero A) +* (x1 .--> 1)) c= (rng (RealFuncZero A)) \/ (rng (x1 .--> 1)) by FUNCT_4:17;
B1: rng (RealFuncZero A) c= REAL by RELAT_1:def 19;
rng (x1 .--> 1) = {1} by FUNCOP_1:8;
then rng (x1 .--> 1) c= REAL by XREAL_0:def 1, ZFMISC_1:31;
then (rng (RealFuncZero A)) \/ (rng (x1 .--> 1)) c= REAL \/ REAL by B1, XBOOLE_1:13;
then S1: (RealFuncZero A) +* (x1 .--> 1) is Function of A,REAL by A2, FUNCT_2:2, H2, XBOOLE_1:1;
H2: rng ((RealFuncUnit A) +* (x1 .--> 0)) c= (rng (RealFuncUnit A)) \/ (rng (x1 .--> 0)) by FUNCT_4:17;
B1: rng (RealFuncUnit A) c= REAL by RELAT_1:def 19;
rng (x1 .--> 0) = {0} by FUNCOP_1:8;
then rng (x1 .--> 0) c= REAL by XREAL_0:def 1, ZFMISC_1:31;
then (rng (RealFuncUnit A)) \/ (rng (x1 .--> 0)) c= REAL \/ REAL by B1, XBOOLE_1:13;
then (RealFuncUnit A) +* (x1 .--> 0) is Function of A,REAL by a2, FUNCT_2:2, H2, XBOOLE_1:1;
hence ( (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL) ) by S1, FUNCT_2:8; :: thesis: verum