let i be Element of SCM+FSA-Instr ; :: thesis: for ii being Element of SCM-Instr st i = ii holds

JumpParts (InsCode i) = JumpParts (InsCode ii)

let ii be Element of SCM-Instr ; :: thesis: ( i = ii implies JumpParts (InsCode i) = JumpParts (InsCode ii) )

assume A1: i = ii ; :: thesis: JumpParts (InsCode i) = JumpParts (InsCode ii)

thus JumpParts (InsCode i) c= JumpParts (InsCode ii) :: according to XBOOLE_0:def 10 :: thesis: JumpParts (InsCode ii) c= JumpParts (InsCode i)

assume e in JumpParts (InsCode ii) ; :: thesis: e in JumpParts (InsCode i)

then consider II being Element of SCM-Instr such that

A4: e = JumpPart II and

A5: InsCode II = InsCode ii ;

A6: SCM-Instr c= SCM+FSA-Instr by Th1;

II in SCM+FSA-Instr by A6;

then reconsider I = II as Element of SCM+FSA-Instr ;

InsCode I = InsCode i by A1, A5;

hence e in JumpParts (InsCode i) by A4; :: thesis: verum

JumpParts (InsCode i) = JumpParts (InsCode ii)

let ii be Element of SCM-Instr ; :: thesis: ( i = ii implies JumpParts (InsCode i) = JumpParts (InsCode ii) )

assume A1: i = ii ; :: thesis: JumpParts (InsCode i) = JumpParts (InsCode ii)

thus JumpParts (InsCode i) c= JumpParts (InsCode ii) :: according to XBOOLE_0:def 10 :: thesis: JumpParts (InsCode ii) c= JumpParts (InsCode i)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in JumpParts (InsCode ii) or e in JumpParts (InsCode i) )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in JumpParts (InsCode i) or e in JumpParts (InsCode ii) )

assume e in JumpParts (InsCode i) ; :: thesis: e in JumpParts (InsCode ii)

then consider I being Element of SCM+FSA-Instr such that

A2: e = JumpPart I and

A3: InsCode I = InsCode i ;

InsCode I <= 8 by A1, A3, SCM_INST:10;

then reconsider II = I as Element of SCM-Instr by Th2;

InsCode II = InsCode ii by A1, A3;

hence e in JumpParts (InsCode ii) by A2; :: thesis: verum

end;assume e in JumpParts (InsCode i) ; :: thesis: e in JumpParts (InsCode ii)

then consider I being Element of SCM+FSA-Instr such that

A2: e = JumpPart I and

A3: InsCode I = InsCode i ;

InsCode I <= 8 by A1, A3, SCM_INST:10;

then reconsider II = I as Element of SCM-Instr by Th2;

InsCode II = InsCode ii by A1, A3;

hence e in JumpParts (InsCode ii) by A2; :: thesis: verum

assume e in JumpParts (InsCode ii) ; :: thesis: e in JumpParts (InsCode i)

then consider II being Element of SCM-Instr such that

A4: e = JumpPart II and

A5: InsCode II = InsCode ii ;

A6: SCM-Instr c= SCM+FSA-Instr by Th1;

II in SCM+FSA-Instr by A6;

then reconsider I = II as Element of SCM+FSA-Instr ;

InsCode I = InsCode i by A1, A5;

hence e in JumpParts (InsCode i) by A4; :: thesis: verum