set f2 = (0 ,0 .--> 0 ) +* (0 ,1 .--> 1);
set f1 = ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1);
set f = (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 );
A1: dom ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 )) =
(dom (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1))) \/ (dom (1,1 .--> 0 ))
by FUNCT_4:def 1
.=
(dom (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1))) \/ {[1,1]}
by FUNCOP_1:19
.=
((dom ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1))) \/ (dom (1,0 .--> 1))) \/ {[1,1]}
by FUNCT_4:def 1
.=
((dom ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1))) \/ {[1,0 ]}) \/ {[1,1]}
by FUNCOP_1:19
.=
(((dom (0 ,0 .--> 0 )) \/ (dom (0 ,1 .--> 1))) \/ {[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
;
A2:
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 A3:
rng (0 ,0 .--> 0 ) c= 2
by A2, XBOOLE_1:1;
A4:
{1} c= 2
by CARD_1:88, ZFMISC_1:12;
rng (0 ,1 .--> 1) c= {1}
by FUNCOP_1:19;
then
rng (0 ,1 .--> 1) c= 2
by A4, XBOOLE_1:1;
then A5:
(rng (0 ,0 .--> 0 )) \/ (rng (0 ,1 .--> 1)) c= 2
by A3, XBOOLE_1:8;
rng (1,0 .--> 1) c= {1}
by FUNCOP_1:19;
then A6:
rng (1,0 .--> 1) c= 2
by A4, XBOOLE_1:1;
rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) c= (rng (0 ,0 .--> 0 )) \/ (rng (0 ,1 .--> 1))
by FUNCT_4:18;
then
rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) c= 2
by A5, XBOOLE_1:1;
then A7:
(rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1))) \/ (rng (1,0 .--> 1)) c= 2
by A6, XBOOLE_1:8;
rng (1,1 .--> 0 ) c= 1
by CARD_1:87, FUNCOP_1:19;
then A8:
rng (1,1 .--> 0 ) c= 2
by A2, XBOOLE_1:1;
rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) c= (rng ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1))) \/ (rng (1,0 .--> 1))
by FUNCT_4:18;
then
rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) c= 2
by A7, XBOOLE_1:1;
then A9:
(rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1))) \/ (rng (1,1 .--> 0 )) c= 2
by A8, XBOOLE_1:8;
rng ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 )) c= (rng (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1))) \/ (rng (1,1 .--> 0 ))
by FUNCT_4:18;
then
rng ((((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 )) c= 2
by A9, XBOOLE_1:1;
hence
(((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) +* (1,1 .--> 0 ) is BinOp of 2
by A1, FUNCT_2:def 1, RELSET_1:11; verum