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 ),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 ),n) --> (n,i) is PartState of S
let n be Nat; :: thesis: for i being Instruction of S holds ((IC ),n) --> (n,i) is PartState of S
let i be Instruction of S; :: thesis: ((IC ),n) --> (n,i) is PartState of S
set p = ((IC ),n) --> (n,i);
A1: n in NAT by ORDINAL1:def 13;
A2: dom (((IC ),n) --> (n,i)) = {(IC ),n} by FUNCT_4:65;
A3: IC <> n by A1, Def12;
((IC ),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 ),n) --> (n,i)) or (((IC ),n) --> (n,i)) . x in the Object-Kind of S . x )
assume A4: x in dom (((IC ),n) --> (n,i)) ; :: thesis: (((IC ),n) --> (n,i)) . x in the Object-Kind of S . x

per cases ( x = IC or x = n ) by A4, A2, TARSKI:def 2;

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

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

end;

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

then A8: (((IC ),n) --> (n,i)) . x = i by FUNCT_4:66;
the Object-Kind of S . x = the Instructions of S by Def8, A7, A1;
hence (((IC ),n) --> (n,i)) . x in the Object-Kind of S . x by A8; :: thesis: verum

end;

end;

end;

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