A10:
rng (1,1 .--> 1) c= {1}
by FUNCOP_1:19;
{1} c= 2
by CARD_1:88, ZFMISC_1:12;
then A11:
rng (1,1 .--> 1) c= 2
by A10, XBOOLE_1:1;
set f2 = (0 ,0 .--> 0 ) +* (0 ,1 .--> 0 );
set f1 = ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 );
set f = (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) +* (1,1 .--> 1);
A12: dom ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) +* (1,1 .--> 1)) =
(dom (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 ))) \/ (dom (1,1 .--> 1))
by FUNCT_4:def 1
.=
(dom (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 ))) \/ {[1,1]}
by FUNCOP_1:19
.=
((dom ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 ))) \/ (dom (1,0 .--> 0 ))) \/ {[1,1]}
by FUNCT_4:def 1
.=
((dom ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 ))) \/ {[1,0 ]}) \/ {[1,1]}
by FUNCOP_1:19
.=
(((dom (0 ,0 .--> 0 )) \/ (dom (0 ,1 .--> 0 ))) \/ {[1,0 ]}) \/ {[1,1]}
by FUNCT_4:def 1
.=
(((dom (0 ,0 .--> 0 )) \/ {[0 ,1]}) \/ {[1,0 ]}) \/ {[1,1]}
by FUNCOP_1:19
.=
(({[0 ,0 ]} \/ {[0 ,1]}) \/ {[1,0 ]}) \/ {[1,1]}
by FUNCOP_1:19
.=
({[0 ,0 ],[0 ,1]} \/ {[1,0 ]}) \/ {[1,1]}
by ENUMSET1:41
.=
{[0 ,0 ],[0 ,1],[1,0 ]} \/ {[1,1]}
by ENUMSET1:43
.=
{[0 ,0 ],[0 ,1],[1,0 ],[1,1]}
by ENUMSET1:46
.=
[:2,2:]
by CARD_1:88, ZFMISC_1:146
;
A13:
1 c= 2
by CARD_1:87, CARD_1:88, ZFMISC_1:12;
rng (0 ,0 .--> 0 ) c= 1
by CARD_1:87, FUNCOP_1:19;
then A14:
rng (0 ,0 .--> 0 ) c= 2
by A13, XBOOLE_1:1;
rng (0 ,1 .--> 0 ) c= 1
by CARD_1:87, FUNCOP_1:19;
then
rng (0 ,1 .--> 0 ) c= 2
by A13, XBOOLE_1:1;
then A15:
(rng (0 ,0 .--> 0 )) \/ (rng (0 ,1 .--> 0 )) c= 2
by A14, XBOOLE_1:8;
rng (1,0 .--> 0 ) c= 1
by CARD_1:87, FUNCOP_1:19;
then A16:
rng (1,0 .--> 0 ) c= 2
by A13, XBOOLE_1:1;
rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) c= (rng (0 ,0 .--> 0 )) \/ (rng (0 ,1 .--> 0 ))
by FUNCT_4:18;
then
rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) c= 2
by A15, XBOOLE_1:1;
then A17:
(rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 ))) \/ (rng (1,0 .--> 0 )) c= 2
by A16, XBOOLE_1:8;
rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) c= (rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 ))) \/ (rng (1,0 .--> 0 ))
by FUNCT_4:18;
then
rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) c= 2
by A17, XBOOLE_1:1;
then A18:
(rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 ))) \/ (rng (1,1 .--> 1)) c= 2
by A11, XBOOLE_1:8;
rng ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) +* (1,1 .--> 1)) c= (rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 ))) \/ (rng (1,1 .--> 1))
by FUNCT_4:18;
then
rng ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) +* (1,1 .--> 1)) c= 2
by A18, XBOOLE_1:1;
hence
(((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) +* (1,1 .--> 1) is BinOp of 2
by A12, FUNCT_2:def 1, RELSET_1:11; verum