let k be Nat; :: thesis: for S being non empty standard-ins homogeneous J/A-independent set
for I being Element of S holds JumpParts () = JumpParts (InsCode (IncAddr (I,k)))

let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I being Element of S holds JumpParts () = JumpParts (InsCode (IncAddr (I,k)))
let I be Element of S; :: thesis: JumpParts () = JumpParts (InsCode (IncAddr (I,k)))
set A = { () where J is Element of S : InsCode I = InsCode J } ;
set B = { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ;
{ (JumpPart J) where J is Element of S : InsCode I = InsCode J } = { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } c= { () where J is Element of S : InsCode I = InsCode J }
let a be object ; :: thesis: ( a in { () where J is Element of S : InsCode I = InsCode J } implies a in { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } )
assume a in { () where J is Element of S : InsCode I = InsCode J } ; :: thesis: a in { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }
then consider J being Element of S such that
A1: a = JumpPart J and
A2: InsCode J = InsCode I ;
InsCode J = InsCode (IncAddr (I,k)) by ;
hence a in { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } by A1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } or a in { () where J is Element of S : InsCode I = InsCode J } )
assume a in { () where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ; :: thesis: a in { () where J is Element of S : InsCode I = InsCode J }
then consider J being Element of S such that
A3: a = JumpPart J and
A4: InsCode J = InsCode (IncAddr (I,k)) ;
InsCode J = InsCode I by ;
hence a in { () where J is Element of S : InsCode I = InsCode J } by A3; :: thesis: verum
end;
hence JumpParts () = JumpParts (InsCode (IncAddr (I,k))) ; :: thesis: verum