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

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

NAT c= (product" (JumpParts (InsCode I))) . x )

assume A1: S is J/A-independent ; :: thesis: for I being Element of S

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

NAT c= (product" (JumpParts (InsCode I))) . x

consider D0 being non empty set such that

A2: S c= [:NAT,(NAT *),(D0 *):] by Def1;

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

NAT c= (product" (JumpParts (InsCode I))) . x

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

assume A3: x in dom (JumpPart I) ; :: thesis: NAT c= (product" (JumpParts (InsCode I))) . x

A4: JumpPart I in JumpParts (InsCode I) ;

then dom (product" (JumpParts (InsCode I))) = dom (JumpPart I) by CARD_3:100;

then A5: (product" (JumpParts (InsCode I))) . x = { (f . x) where f is Element of JumpParts (InsCode I) : verum } by A3, CARD_3:74;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in NAT or e in (product" (JumpParts (InsCode I))) . x )

assume e in NAT ; :: thesis: e in (product" (JumpParts (InsCode I))) . x

then reconsider e = e as Element of NAT ;

set g = (JumpPart I) +* (x,e);

A6: dom ((JumpPart I) +* (x,e)) = dom (JumpPart I) by FUNCT_7:30;

I in S ;

then [(InsCode I),(JumpPart I),(AddressPart I)] in S by A2, RECDEF_2:3;

then reconsider J = [(InsCode I),((JumpPart I) +* (x,e)),(AddressPart I)] as Element of S by A4, A1, A6;

InsCode J = InsCode I ;

then JumpPart J in JumpParts (InsCode I) ;

then reconsider g = (JumpPart I) +* (x,e) as Element of JumpParts (InsCode I) ;

e = g . x by A3, FUNCT_7:31;

hence e in (product" (JumpParts (InsCode I))) . x by A5; :: thesis: verum

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

NAT c= (product" (JumpParts (InsCode I))) . x )

assume A1: S is J/A-independent ; :: thesis: for I being Element of S

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

NAT c= (product" (JumpParts (InsCode I))) . x

consider D0 being non empty set such that

A2: S c= [:NAT,(NAT *),(D0 *):] by Def1;

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

NAT c= (product" (JumpParts (InsCode I))) . x

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

assume A3: x in dom (JumpPart I) ; :: thesis: NAT c= (product" (JumpParts (InsCode I))) . x

A4: JumpPart I in JumpParts (InsCode I) ;

then dom (product" (JumpParts (InsCode I))) = dom (JumpPart I) by CARD_3:100;

then A5: (product" (JumpParts (InsCode I))) . x = { (f . x) where f is Element of JumpParts (InsCode I) : verum } by A3, CARD_3:74;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in NAT or e in (product" (JumpParts (InsCode I))) . x )

assume e in NAT ; :: thesis: e in (product" (JumpParts (InsCode I))) . x

then reconsider e = e as Element of NAT ;

set g = (JumpPart I) +* (x,e);

A6: dom ((JumpPart I) +* (x,e)) = dom (JumpPart I) by FUNCT_7:30;

I in S ;

then [(InsCode I),(JumpPart I),(AddressPart I)] in S by A2, RECDEF_2:3;

then reconsider J = [(InsCode I),((JumpPart I) +* (x,e)),(AddressPart I)] as Element of S by A4, A1, A6;

InsCode J = InsCode I ;

then JumpPart J in JumpParts (InsCode I) ;

then reconsider g = (JumpPart I) +* (x,e) as Element of JumpParts (InsCode I) ;

e = g . x by A3, FUNCT_7:31;

hence e in (product" (JumpParts (InsCode I))) . x by A5; :: thesis: verum