consider A being non empty set , T being Function of [:A,I:],A, o being Function of A,O, I being Element of A, F being Subset of A;
take S = Moore-SM_Final(# A,T,o,I,F #); :: thesis: ( not S is empty & S is strict )
thus not the carrier of S is empty ; :: according to STRUCT_0:def 1 :: thesis: S is strict
thus S is strict ; :: thesis: verum