let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-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 COM-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;
U: dom (((IC S),n) --> (n,i)) = {(IC S),n} by FUNCT_4:65;
V: IC S <> n by y, Def21;
((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, S, ORDINAL1:def 13; :: 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 Def8, 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 ; :: thesis: verum