let I be Instruction of (SCM R); :: according to COMPOS_1:def 14 :: thesis:
set T = InsCode I;
A1: JumpPart I in JumpParts (InsCode I) ;

per cases by Lm2;

suppose InsCode I = 0 ; :: thesis:

then I = halt (SCM R) by Th16;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 1 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th33;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 2 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th34;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 3 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th35;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 4 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th36;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose InsCode I = 5 ; :: thesis:

then JumpParts (InsCode I) = {{}} by Th37;
then JumpPart I = {} by A1, TARSKI:def 1;
hence for b₁ being set holds
( not b₁ in dom (I `2_3) or (product" (JumpParts (InsCode I))) . b₁ = NAT ) ; :: thesis:

end;

suppose A2: InsCode I = 6 ; :: thesis:

then consider i2 being Element of NAT such that
A3: I = goto (i2,R) by Th22;
let k be set ; :: thesis:
assume A4: k in dom (JumpPart I) ; :: thesis:
for f being Function st f in JumpParts (InsCode I) holds
k in dom f

proof

let f be Function; :: thesis:
assume f in JumpParts (InsCode I) ; :: thesis:
then consider J being Instruction of (SCM R) such that
A5: f = JumpPart J and
A6: InsCode J = InsCode I ;
thus k in dom f by A4, A5, A6, COMPOS_1:def 12; :: thesis:

end;

then k in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then k in {1} by A2, Th38;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A3, Th50; :: thesis:

end;

suppose A7: InsCode I = 7 ; :: thesis:

then consider a being Data-Location of R, i1 being Element of NAT such that
A8: I = a =0_goto i1 by Th23;
let k be set ; :: thesis:
assume A9: k in dom (JumpPart I) ; :: thesis:
for f being Function st f in JumpParts (InsCode I) holds
k in dom f

proof

let f be Function; :: thesis:
assume f in JumpParts (InsCode I) ; :: thesis:
then consider J being Instruction of (SCM R) such that
A10: f = JumpPart J and
A11: InsCode J = InsCode I ;
thus k in dom f by A9, A10, A11, COMPOS_1:def 12; :: thesis:

end;

then k in dom (product" (JumpParts (InsCode I))) by CARD_3:def 12;
then k in {1} by A7, Th39;
then k = 1 by TARSKI:def 1;
hence (product" (JumpParts (InsCode I))) . k = NAT by A8, Th51; :: thesis:

end;

end;