thus
SCM+FSA-Instr is standard-ins
:: thesis: not SCM+FSA-Instr is empty

proof

thus
not SCM+FSA-Instr is empty
; :: thesis: verum
consider X being non empty set such that

A1: proj2 SCM+FSA-Instr c= X * by FINSEQ_1:85;

take X ; :: according to COMPOS_0:def 1 :: thesis: SCM+FSA-Instr c= [:NAT,(NAT *),(X *):]

[:NAT,(NAT *),(proj2 SCM+FSA-Instr):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;

hence SCM+FSA-Instr c= [:NAT,(NAT *),(X *):] by Lm1; :: thesis: verum

end;A1: proj2 SCM+FSA-Instr c= X * by FINSEQ_1:85;

take X ; :: according to COMPOS_0:def 1 :: thesis: SCM+FSA-Instr c= [:NAT,(NAT *),(X *):]

[:NAT,(NAT *),(proj2 SCM+FSA-Instr):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;

hence SCM+FSA-Instr c= [:NAT,(NAT *),(X *):] by Lm1; :: thesis: verum