thus not the carrier of SCM+FSA is empty ; :: according to STRUCT_0:def 1 :: thesis: ( SCM+FSA is stored-program & SCM+FSA is standard-ins )
thus NAT c= the carrier of SCM+FSA ; :: according to COMPOS_1:def 2 :: thesis: SCM+FSA is standard-ins
consider X being non empty set such that
WW: proj2 SCM+FSA-Instr c= X * by FINSEQ_1:106;
take X ; :: according to COMPOS_1:def 17 :: thesis: the Instructions of SCM+FSA c= [:K99(),(K99() * ),(X * ):]
S: SCM+FSA-Instr c= [:NAT ,(NAT * ),(proj2 SCM+FSA-Instr ):] by SCMFSA_1:34;
[:NAT ,(NAT * ),(proj2 SCM+FSA-Instr ):] c= [:NAT ,(NAT * ),(X * ):] by WW, MCART_1:77;
then SCM+FSA-Instr c= [:NAT ,(NAT * ),(X * ):] by S, XBOOLE_1:1;
hence the Instructions of SCM+FSA c= [:NAT ,(NAT * ),(X * ):] ; :: thesis: verum