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

let I be Element of S; :: thesis: IncAddr (I,0) = I

A1: InsCode (IncAddr (I,0)) = InsCode I by Def8;

A2: AddressPart (IncAddr (I,0)) = AddressPart I by Def8;

A3: JumpPart (IncAddr (I,0)) = 0 + (JumpPart I) by Def8;

then A4: dom (JumpPart I) = dom (JumpPart (IncAddr (I,0))) by VALUED_1:def 2;

for k being Nat st k in dom (JumpPart I) holds

(JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k

hence IncAddr (I,0) = I by A1, A2, Th1; :: thesis: verum

let I be Element of S; :: thesis: IncAddr (I,0) = I

A1: InsCode (IncAddr (I,0)) = InsCode I by Def8;

A2: AddressPart (IncAddr (I,0)) = AddressPart I by Def8;

A3: JumpPart (IncAddr (I,0)) = 0 + (JumpPart I) by Def8;

then A4: dom (JumpPart I) = dom (JumpPart (IncAddr (I,0))) by VALUED_1:def 2;

for k being Nat st k in dom (JumpPart I) holds

(JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k

proof

then
JumpPart (IncAddr (I,0)) = JumpPart I
by A4;
let k be Nat; :: thesis: ( k in dom (JumpPart I) implies (JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k )

assume k in dom (JumpPart I) ; :: thesis: (JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k

hence (JumpPart (IncAddr (I,0))) . k = 0 + ((JumpPart I) . k) by A4, A3, VALUED_1:def 2

.= (JumpPart I) . k ;

:: thesis: verum

end;assume k in dom (JumpPart I) ; :: thesis: (JumpPart (IncAddr (I,0))) . k = (JumpPart I) . k

hence (JumpPart (IncAddr (I,0))) . k = 0 + ((JumpPart I) . k) by A4, A3, VALUED_1:def 2

.= (JumpPart I) . k ;

:: thesis: verum

hence IncAddr (I,0) = I by A1, A2, Th1; :: thesis: verum