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 ,IAlph:],OAlph;
set I = the Element of the non empty finite set ;
take Mealy-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 ,IAlph:],OAlph, the Element of the non empty finite set #) ; :: thesis: ( Mealy-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 ,IAlph:],OAlph, the Element of the non empty finite set #) is finite & not Mealy-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 ,IAlph:],OAlph, the Element of the non empty finite set #) is empty )
thus ( Mealy-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 ,IAlph:],OAlph, the Element of the non empty finite set #) is finite & not Mealy-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 ,IAlph:],OAlph, the Element of the non empty finite set #) is empty ) ; :: thesis: verum