[(In 0 ,2),(In 0 ,2)] <> [0 ,1]
by Lm3, ZFMISC_1:33;
then A1:
not [(In 0 ,2),(In 0 ,2)] in dom (0 ,1 .--> 0 )
by Lm14, TARSKI:def 1;
[(In 0 ,2),(In 0 ,2)] <> [1,0 ]
by Lm3, ZFMISC_1:33;
then A2:
not [(In 0 ,2),(In 0 ,2)] in dom (1,0 .--> 0 )
by Lm13, TARSKI:def 1;
[(In 0 ,2),(In 0 ,2)] <> [1,1]
by Lm3, ZFMISC_1:33;
then
not [(In 0 ,2),(In 0 ,2)] in dom (1,1 .--> 1)
by Lm12, TARSKI:def 1;
hence mult_2 . (In 0 ,2),(In 0 ,2) =
(((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) +* (1,0 .--> 0 )) . (In 0 ,2),(In 0 ,2)
by FUNCT_4:12
.=
((0 ,0 .--> 0 ) +* (0 ,1 .--> 0 )) . (In 0 ,2),(In 0 ,2)
by A2, FUNCT_4:12
.=
(0 ,0 .--> 0 ) . (In 0 ,2),(In 0 ,2)
by A1, FUNCT_4:12
.=
In 0 ,2
by Lm3, FUNCOP_1:86
;
verum