2 in NAT ;
then B0: 2 in INT by NUMBERS:17;
for x, x1, y being set holds
( not x in NAT or not x1 in NAT * or not y in proj2 SCM+FSA-Instr or not 2 = [x,x1,y] ) ;
then not 2 in [:NAT ,(NAT * ),(proj2 SCM+FSA-Instr ):] by MCART_1:72;
then A2: not 2 in SCM+FSA-Instr by LmX;
hence SCM+FSA-Instr <> INT by B0; :: thesis: ( NAT <> SCM+FSA-Instr & NAT <> INT * & SCM+FSA-Instr <> INT * )
thus NAT <> SCM+FSA-Instr by A2; :: thesis: ( NAT <> INT * & SCM+FSA-Instr <> INT * )
0 in INT by INT_1:def 1;
then <*0 *> is FinSequence of INT by FINSEQ_1:95;
then A2: <*0 *> in INT * by FINSEQ_1:def 11;

hereby :: thesis: SCM+FSA-Instr <> INT *

A3: card <*0 *> = 1 by CARD_1:50;
assume NAT = INT * ; :: thesis: contradiction
then <*0 *> = {0 } by A2, A3, CARD_1:87, CARD_1:def 5;
hence contradiction by ZFMISC_1:6; :: thesis: verum

end;

now

assume {} in SCM+FSA-Instr ; :: thesis: contradiction
then {} in [:NAT ,(NAT * ),(proj2 SCM+FSA-Instr ):] by LmX;
then ex x, x1, y being set st
( x in NAT & x1 in NAT * & y in proj2 SCM+FSA-Instr & {} = [x,x1,y] ) by MCART_1:72;
hence contradiction ; :: thesis: verum

end;

hence SCM+FSA-Instr <> INT * by FINSEQ_1:66; :: thesis: verum