let T be InsType of SCMPDS-Instr; COMPOS_0:def 7 for b1, b2 being set holds
( not b1 in JumpParts T or not proj1 b1 = proj1 b2 or for b3 being object holds
( not [T,b1,b3] in SCMPDS-Instr or [T,b2,b3] in SCMPDS-Instr ) )
let f1, f2 be natural-valued Function; ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b1 being object holds
( not [T,f1,b1] in SCMPDS-Instr or [T,f2,b1] in SCMPDS-Instr ) )
assume that
A1:
f1 in JumpParts T
and
A2:
dom f1 = dom f2
; for b1 being object holds
( not [T,f1,b1] in SCMPDS-Instr or [T,f2,b1] in SCMPDS-Instr )
let p be object ; ( not [T,f1,p] in SCMPDS-Instr or [T,f2,p] in SCMPDS-Instr )
assume A3:
[T,f1,p] in SCMPDS-Instr
; [T,f2,p] in SCMPDS-Instr
reconsider i = [T,f1,p] as Element of SCMPDS-Instr by A3;
not not InsCode i = 0 & ... & not InsCode i = 14
by Lm2, NAT_1:60;
then A4:
JumpPart i = {}
by Lm4, Lm5, Lm6, Lm7, Lm8, Lm3;
T = InsCode i
;
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; verum