set X = {i,f};
reconsider ii = i, ff = f as Element of {i,f} by TARSKI:def 2;
reconsider oo = o as Function of {i,f},O ;
not Moore-SM_Final(# {i,f},([:{i,f},I:] --> ff),oo,ii,{ff} #) is empty ;
hence ex b₁ being non empty strict Moore-SM_Final over I,O st
( the carrier of b₁ = {i,f} & the Tran of b₁ = [:{i,f},I:] --> f & the OFun of b₁ = o & the InitS of b₁ = i & the FinalS of b₁ = {f} ) ; :: thesis: verum