A1:
[(In (1,2)),(In (0,2))] in dom ((1,0) .--> 0)
by Lm3, Lm4, Lm13, TARSKI:def 1;
[(In (1,2)),(In (0,2))] <> [1,1]
by Lm3, ZFMISC_1:33;
then
not [(In (1,2)),(In (0,2))] in dom ((1,1) .--> 1)
by Lm12, TARSKI:def 1;
hence mult_2 . ((In (1,2)),(In (0,2))) =
((((0,0) .--> 0) +* ((0,1) .--> 0)) +* ((1,0) .--> 0)) . ((In (1,2)),(In (0,2)))
by FUNCT_4:12
.=
((1,0) .--> 0) . ((In (1,2)),(In (0,2)))
by A1, FUNCT_4:14
.=
In (0,2)
by Lm3, Lm4, FUNCOP_1:86
;
verum