let T be InsType of SCMPDS-Instr; :: according to COMPOS_0:def 7 :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in JumpParts T or not proj1 b_{1} = proj1 b_{2} or for b_{3} being object holds

( not [T,b_{1},b_{3}] in SCMPDS-Instr or [T,b_{2},b_{3}] 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_{1} being object holds

( not [T,f1,b_{1}] in SCMPDS-Instr or [T,f2,b_{1}] in SCMPDS-Instr ) )

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for b_{1} being object holds

( not [T,f1,b_{1}] in SCMPDS-Instr or [T,f2,b_{1}] in SCMPDS-Instr )

let p be object ; :: 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;

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; :: thesis: verum

( not b

( not [T,b

let f1, f2 be natural-valued Function; :: thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b

( not [T,f1,b

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for b

( not [T,f1,b

let p be object ; :: 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;

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; :: thesis: verum