let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for n being Nat
for i being Instruction of S holds (IC S),n --> n,i is PartState of S
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for n being Nat
for i being Instruction of S holds (IC S),n --> n,i is PartState of S
let n be Nat; :: thesis: for i being Instruction of S holds (IC S),n --> n,i is PartState of S
let i be Instruction of S; :: thesis: (IC S),n --> n,i is PartState of S
set p = (IC S),n --> n,i;
y: n in NAT by ORDINAL1:def 13;
Y: NAT c= the carrier of S by Def3;
U: dom ((IC S),n --> n,i) = {(IC S),n} by FUNCT_4:65;
V: IC S <> n by y, Def21;
A: (IC S),n --> n,i is the carrier of S -defined

proof

thus dom ((IC S),n --> n,i) c= the carrier of S by Y, ZFMISC_1:38, U, y; :: according to RELAT_1:def 18 :: thesis: verum

end;

(IC S),n --> n,i is the Object-Kind of S -compatible

proof

let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in proj1 ((IC S),n --> n,i) or ((IC S),n --> n,i) . x in the Object-Kind of S . x )
assume Z: x in dom ((IC S),n --> n,i) ; :: thesis: ((IC S),n --> n,i) . x in the Object-Kind of S . x

per cases ( x = IC S or x = n ) by Z, U, TARSKI:def 2;

suppose S: x = IC S ; :: thesis: ((IC S),n --> n,i) . x in the Object-Kind of S . x

then I: ((IC S),n --> n,i) . x = n by V, FUNCT_4:66;
ObjectKind (IC S) = NAT by Def11;
hence ((IC S),n --> n,i) . x in the Object-Kind of S . x by I, ORDINAL1:def 13, S; :: thesis: verum

end;

suppose S: x = n ; :: thesis: ((IC S),n --> n,i) . x in the Object-Kind of S . x

then I: ((IC S),n --> n,i) . x = i by FUNCT_4:66;
the Object-Kind of S . x = the Instructions of S by Def14, S, y;
hence ((IC S),n --> n,i) . x in the Object-Kind of S . x by I; :: thesis: verum

end;

end;

end;

hence (IC S),n --> n,i is PartState of S by A; :: thesis: verum