A1:
[(In (1,2)),(In (0,2))] in dom ((1,0) .--> 1)
by Lm3, Lm4, Lm6, 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) .--> 0)
by Lm5, TARSKI:def 1;
hence add_2 . ((In (1,2)),(In (0,2))) =
((((0,0) .--> 0) +* ((0,1) .--> 1)) +* ((1,0) .--> 1)) . ((In (1,2)),(In (0,2)))
by FUNCT_4:12
.=
((1,0) .--> 1) . ((In (1,2)),(In (0,2)))
by A1, FUNCT_4:14
.=
In (1,2)
by Lm3, Lm4, FUNCOP_1:86
;
verum