[(In 0 ,2),(In 1,2)] <> [1,1] by Lm2, ZFMISC_1:33;
then A1: not [(In 0 ,2),(In 1,2)] in dom (1,1 .--> 0 ) by Lm3, TARSKI:def 1;
[(In 0 ,2),(In 1,2)] <> [1,0 ] by Lm2, ZFMISC_1:33;
then A2: not [(In 0 ,2),(In 1,2)] in dom (1,0 .--> 1) by Lm4, TARSKI:def 1;
A3: [(In 0 ,2),(In 1,2)] in dom (0 ,1 .--> 1) by Lm2, Lm5, TARSKI:def 1;
thus add_2 . (In 0 ,2),(In 1,2) = (((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) +* (1,0 .--> 1)) . (In 0 ,2),(In 1,2) by A1, FUNCT_4:12
.= ((0 ,0 .--> 0 ) +* (0 ,1 .--> 1)) . (In 0 ,2),(In 1,2) by A2, FUNCT_4:12
.= (0 ,1 .--> 1) . (In 0 ,2),(In 1,2) by A3, FUNCT_4:14
.= In 1,2 by Lm2, FUNCOP_1:86 ; :: thesis: verum