consider X being non empty set such that
A1: proj2 (SCM-Instr R) c= X * by FINSEQ_1:85;
take X ; :: according to COMPOS_0:def 1 :: thesis: SCM-Instr R c= [:NAT,(NAT *),(X *):]
A2: SCM-Instr R c= [:NAT,(NAT *),(proj2 (SCM-Instr R)):] by Th5;
[:NAT,(NAT *),(proj2 (SCM-Instr R)):] c= [:NAT,(NAT *),(X *):] by A1, MCART_1:73;
hence SCM-Instr R c= [:NAT,(NAT *),(X *):] by A2; :: thesis: verum