set X = the non empty finite set ;
set T = the Function of [: the non empty finite set ,IAlph:], the non empty finite set ;
set O = the Function of the non empty finite set ,OAlph;
set I = the Element of the non empty finite set ;
take Moore-FSM(# the non empty finite set , the Function of [: the non empty finite set ,IAlph:], the non empty finite set , the Function of the non empty finite set ,OAlph, the Element of the non empty finite set #) ; :: thesis: ( Moore-FSM(# the non empty finite set , the Function of [: the non empty finite set ,IAlph:], the non empty finite set , the Function of the non empty finite set ,OAlph, the Element of the non empty finite set #) is finite & not Moore-FSM(# the non empty finite set , the Function of [: the non empty finite set ,IAlph:], the non empty finite set , the Function of the non empty finite set ,OAlph, the Element of the non empty finite set #) is empty )
thus ( Moore-FSM(# the non empty finite set , the Function of [: the non empty finite set ,IAlph:], the non empty finite set , the Function of the non empty finite set ,OAlph, the Element of the non empty finite set #) is finite & not Moore-FSM(# the non empty finite set , the Function of [: the non empty finite set ,IAlph:], the non empty finite set , the Function of the non empty finite set ,OAlph, the Element of the non empty finite set #) is empty ) ; :: thesis: verum