thus not the carrier of SCM+FSA is empty ; :: according to STRUCT_0:def 1 :: thesis: SCM+FSA is standard-ins
consider X being non empty set such that
A1: proj2 SCM+FSA-Instr c= X * by FINSEQ_1:85;
take X ; :: according to COMPOS_1:def 4 :: thesis: the Instructions of SCM+FSA c= [:NAT,(NAT *),(X *):]
[:NAT,(NAT *),(proj2 SCM+FSA-Instr):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;
hence the Instructions of SCM+FSA c= [:NAT,(NAT *),(X *):] by SCMFSA_1:31, XBOOLE_1:1; :: thesis: verum