uInt . (1 + 0) = [{(uInt . 0)},{}] by Def1
.= [{0_No},{}] by Def1 ;
hence uInt . 1 = 1_No ; :: thesis: verum