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 ;
:: thesis: verum