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

per cases by Lm3;

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 X, 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 X, 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 X, 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 X, 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 X, 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 A122: InsCode I = 6 ; :: thesis:

then consider i2 being Element of NAT such that
W: I = goto (i2,R) by Th22;
let k be set ; :: thesis:
assume Z: 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
W1: f = JumpPart J and
W2: InsCode J = InsCode I ;
thus k in dom f by Z, W1, W2, COMPOS_1:def 33; :: thesis:

end;

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

end;

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

then consider a being Data-Location of R, i1 being Element of NAT such that
W: I = a =0_goto i1 by Th23;
let k be set ; :: thesis:
assume Z: 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
W1: f = JumpPart J and
W2: InsCode J = InsCode I ;
thus k in dom f by Z, W1, W2, COMPOS_1:def 33; :: thesis:

end;

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

end;

end;