let T be InsType of SCM+FSA-Instr; :: according to COMPOS_0:def 7 :: thesis: for b₁, b₂ being set holds
( not b₁ in JumpParts T or not proj1 b₁ = proj1 b₂ or for b₃ being object holds
( not [T,b₁,b₃] in SCM+FSA-Instr or [T,b₂,b₃] in SCM+FSA-Instr ) )
let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b₁ being object holds
( not [T,f1,b₁] in SCM+FSA-Instr or [T,f2,b₁] in SCM+FSA-Instr ) )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; :: thesis: for b₁ being object holds
( not [T,f1,b₁] in SCM+FSA-Instr or [T,f2,b₁] in SCM+FSA-Instr )
let p be object ; :: thesis: ( not [T,f1,p] in SCM+FSA-Instr or [T,f2,p] in SCM+FSA-Instr )
assume A3: [T,f1,p] in SCM+FSA-Instr ; :: thesis: [T,f2,p] in SCM+FSA-Instr
reconsider II = [T,f1,p] as Element of SCM+FSA-Instr by A3;
InsCode II <= 12 by Lm2;
then not not InsCode II = 0 & ... & not InsCode II = 12 by NAT_1:60;

per cases then ( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 or T = 9 or T = 10 or T = 11 or T = 12 ) ;

suppose ( InsCode II = 0 or InsCode II = 1 or InsCode II = 2 or InsCode II = 3 or InsCode II = 4 or InsCode II = 5 or InsCode II = 6 or InsCode II = 7 or InsCode II = 8 ) ; :: thesis: [T,f2,p] in SCM+FSA-Instr

then A4: InsCode II <= 8 ;
then reconsider ii = II as Element of SCM-Instr by Th2;
A5: T = InsCode ii ;
then T in InsCodes SCM-Instr ;
then reconsider t = T as InsType of SCM-Instr ;
A6: [t,f1,p] in SCM-Instr by A4, Th2;
JumpParts t = JumpParts T by A5, Lm5;
then [t,f2,p] in SCM-Instr by A1, A2, A6, COMPOS_0:def 7;
then [T,f2,p] in SCM-Instr ;
hence [T,f2,p] in SCM+FSA-Instr by Th1; :: thesis: verum

end;

suppose ( T = 9 or T = 10 or T = 11 or T = 12 ) ; :: thesis: [T,f2,p] in SCM+FSA-Instr

then JumpParts T = {0} by Th8, Th9;
then f1 = 0 by A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCM+FSA-Instr by A3; :: thesis: verum

end;

end;