[(In 1,2),(In 1,2)] in dom (1,1 .--> 0 ) by Lm2, Lm3, TARSKI:def 1;
hence add_2 . (In 1,2),(In 1,2) = (1,1 .--> 0 ) . (In 1,2),(In 1,2) by FUNCT_4:14
.= In 0 ,2 by Lm2, FUNCOP_1:86 ;
:: thesis: verum