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