let T be InsType of SCMPDS-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 set holds
( not [T,b₁,b₃] in SCMPDS-Instr or [T,b₂,b₃] in SCMPDS-Instr ) )
let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b₁ being set holds
( not [T,f1,b₁] in SCMPDS-Instr or [T,f2,b₁] in SCMPDS-Instr ) )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; :: thesis: for b₁ being set holds
( not [T,f1,b₁] in SCMPDS-Instr or [T,f2,b₁] in SCMPDS-Instr )
let p be set ; :: thesis: ( not [T,f1,p] in SCMPDS-Instr or [T,f2,p] in SCMPDS-Instr )
assume A3: [T,f1,p] in SCMPDS-Instr ; :: thesis: [T,f2,p] in SCMPDS-Instr
reconsider i = [T,f1,p] as Element of SCMPDS-Instr by A3;
( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 or InsCode i = 14 ) by Lm2, NAT_1:60;
then A4: JumpPart i = {} by Lm4, Lm5, Lm6, Lm7, Lm8, Lm3;
T = InsCode i by RECDEF_2:def 1;
then A5: JumpParts T = {0} by A4, COMPOS_0:11;
f1 = 0 by A5, A1, TARSKI:def 1;
then f1 = f2 by A2;
hence [T,f2,p] in SCMPDS-Instr by A3; :: thesis: verum