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:13
.=
((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:13
.=
(((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:13
.=
(({[0,0]} \/ {[0,1]}) \/ {[1,0]}) \/ {[1,1]}
by FUNCOP_1:13
.=
({[0,0],[0,1]} \/ {[1,0]}) \/ {[1,1]}
by ENUMSET1:1
.=
{[0,0],[0,1],[1,0]} \/ {[1,1]}
by ENUMSET1:3
.=
{[0,0],[0,1],[1,0],[1,1]}
by ENUMSET1:6
.=
[:2,2:]
by CARD_1:50, ZFMISC_1:122
;
A2:
1 c= 2
by CARD_1:49, CARD_1:50, ZFMISC_1:7;
rng ((0,0) .--> 0) c= 1
by CARD_1:49, FUNCOP_1:13;
then A3:
rng ((0,0) .--> 0) c= 2
by A2;
A4:
{1} c= 2
by CARD_1:50, ZFMISC_1:7;
rng ((0,1) .--> 1) c= {1}
by FUNCOP_1:13;
then
rng ((0,1) .--> 1) c= 2
by A4;
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:13;
then A6:
rng ((1,0) .--> 1) c= 2
by A4;
rng (((0,0) .--> 0) +* ((0,1) .--> 1)) c= (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 1))
by FUNCT_4:17;
then
rng (((0,0) .--> 0) +* ((0,1) .--> 1)) c= 2
by A5;
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:49, FUNCOP_1:13;
then A8:
rng ((1,1) .--> 0) c= 2
by A2;
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:17;
then
rng ((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) c= 2
by A7;
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:17;
then
rng (((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) +* ((1,1) .--> 0)) c= 2
by A9;
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:4; verum