thus NAT <> INT by NUMBERS:27; :: thesis: ( SCM+FSA-Instr <> INT & NAT <> SCM+FSA-Instr & NAT <> INT * & SCM+FSA-Instr <> INT * )
A1: for x, y being set holds not 2 = [x,y] ;
thus SCM+FSA-Instr <> INT by A1, NUMBERS:17, RELAT_1:def 1; :: thesis: ( NAT <> SCM+FSA-Instr & NAT <> INT * & SCM+FSA-Instr <> INT * )
thus NAT <> SCM+FSA-Instr by A1, RELAT_1:def 1; :: 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 *

assume NAT = INT * ; :: thesis: contradiction
then A3: ex k being Element of NAT st <*0 *> = k by A2;
card <*0 *> = 1 by CARD_1:50;
then <*0 *> = {0 } by 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 consider x, y being set such that
A4: {} = [x,y] by RELAT_1:def 1;
thus contradiction by A4; :: thesis: verum

end;

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