set f = the Function of {0,1},O;
take I -TwoStatesMooreSM (0,1, the Function of {0,1},O) ; :: thesis: ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting )
thus ( I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is calculating_type & I -TwoStatesMooreSM (0,1, the Function of {0,1},O) is halting ) ; :: thesis: verum