A10:
rng ((1,1) .--> 1) c= {1}
by FUNCOP_1:13;
{1} c= 2
by CARD_1:50, ZFMISC_1:7;
then A11:
rng ((1,1) .--> 1) c= 2
by A10;
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:13
.=
((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:13
.=
(((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: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
;
A13:
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 A14:
rng ((0,0) .--> 0) c= 2
by A13;
rng ((0,1) .--> 0) c= 1
by CARD_1:49, FUNCOP_1:13;
then
rng ((0,1) .--> 0) c= 2
by A13;
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:49, FUNCOP_1:13;
then A16:
rng ((1,0) .--> 0) c= 2
by A13;
rng (((0,0) .--> 0) +* ((0,1) .--> 0)) c= (rng ((0,0) .--> 0)) \/ (rng ((0,1) .--> 0))
by FUNCT_4:17;
then
rng (((0,0) .--> 0) +* ((0,1) .--> 0)) c= 2
by A15;
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:17;
then
rng ((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) c= 2
by A17;
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:17;
then
rng (((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) +* ((1,1) .--> 1)) c= 2
by A18;
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:4; verum