let S be non empty standard-ins homogeneous set ; :: thesis: for I being Element of S
for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
let I be Element of S; :: thesis: for x being set st x in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . x c= NAT
let x be set ; :: thesis: ( x in dom (JumpPart I) implies (product" (JumpParts (InsCode I))) . x c= NAT )
assume A1: x in dom (JumpPart I) ; :: thesis: (product" (JumpParts (InsCode I))) . x c= NAT
JumpPart I in JumpParts (InsCode I) ;
then dom (product" (JumpParts (InsCode I))) = dom (JumpPart I) by CARD_3:100;
then A2: (product" (JumpParts (InsCode I))) . x = { (f . x) where f is Element of JumpParts (InsCode I) : verum } by A1, CARD_3:74;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in (product" (JumpParts (InsCode I))) . x or e in NAT )
assume e in (product" (JumpParts (InsCode I))) . x ; :: thesis: e in NAT
then consider f being Element of JumpParts (InsCode I) such that
A3: e = f . x by A2;
f in JumpParts (InsCode I) ;
then ex J being Element of S st
( f = JumpPart J & InsCode J = InsCode I ) ;
hence e in NAT by A3, ORDINAL1:def 12; :: thesis: verum