[(In (1,2)),(In (1,2))] in dom ((1,1) .--> 0) by Lm4, Lm5, TARSKI:def 1;
hence add_2 . ((In (1,2)),(In (1,2))) = ((1,1) .--> 0) . ((In (1,2)),(In (1,2))) by FUNCT_4:13
.= In (0,2) by Lm3, Lm4, FUNCOP_1:71 ;
:: thesis: verum