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