2 in NAT ;
then B0: 2 in INT by NUMBERS:17;
for x, y being set holds not 2 = [x,y] ;
then not 2 in [:NAT ,(proj2 SCM+FSA-Instr ):] by RELAT_1:def 1;
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 ,(proj2 SCM+FSA-Instr ):] by LmX;
then ex x, y being set st {} = [x,y] by RELAT_1:def 1;
hence contradiction ; :: thesis: verum

end;

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