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