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

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