thus not the carrier of SCM+FSA is empty ; :: according to STRUCT_0:def 1 :: thesis: SCM+FSA is with_non-empty_values
thus the_Values_of SCM+FSA is non-empty ; :: according to MEMSTR_0:def 3 :: thesis: verum