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