[(In (0,2)),(In (0,2))] <> [0,1]
by Lm3, XTUPLE_0:1;
then A1:
not [(In (0,2)),(In (0,2))] in dom ((0,1) .--> 0)
by Lm14, TARSKI:def 1;
[(In (0,2)),(In (0,2))] <> [1,0]
by Lm3, XTUPLE_0:1;
then A2:
not [(In (0,2)),(In (0,2))] in dom ((1,0) .--> 0)
by Lm13, TARSKI:def 1;
[(In (0,2)),(In (0,2))] <> [1,1]
by Lm3, XTUPLE_0:1;
then
not [(In (0,2)),(In (0,2))] in dom ((1,1) .--> 1)
by Lm12, TARSKI:def 1;
hence mult_2 . ((In (0,2)),(In (0,2))) =
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (0,2)),(In (0,2)))
by FUNCT_4:11
.=
(((0,0) .--> 0) +* ((0,1) .--> 0)) . ((In (0,2)),(In (0,2)))
by A2, FUNCT_4:11
.=
((0,0) .--> 0) . ((In (0,2)),(In (0,2)))
by A1, FUNCT_4:11
.=
In (0,2)
by Lm3, FUNCOP_1:71
;
verum