let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I being Element of S

for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

let I be Element of S; :: thesis: for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

let x be set ; :: thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x )

assume A1: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

A2: JumpPart I in JumpParts (InsCode I) ;

A3: dom (product" (JumpParts (InsCode I))) = DOM (JumpParts (InsCode I)) by CARD_3:def 12

.= dom (JumpPart I) by A2, CARD_3:108 ;

(JumpPart I) . x in pi ((JumpParts (InsCode I)),x) by A2, CARD_3:def 6;

hence (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x by A1, A3, CARD_3:def 12; :: thesis: verum

for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

let I be Element of S; :: thesis: for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

let x be set ; :: thesis: ( x in dom (JumpPart I) implies (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x )

assume A1: x in dom (JumpPart I) ; :: thesis: (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

A2: JumpPart I in JumpParts (InsCode I) ;

A3: dom (product" (JumpParts (InsCode I))) = DOM (JumpParts (InsCode I)) by CARD_3:def 12

.= dom (JumpPart I) by A2, CARD_3:108 ;

(JumpPart I) . x in pi ((JumpParts (InsCode I)),x) by A2, CARD_3:def 6;

hence (JumpPart I) . x in (product" (JumpParts (InsCode I))) . x by A1, A3, CARD_3:def 12; :: thesis: verum