B: NAT c= the carrier of S by AMI_1:def 3;
C: dom p c= NAT by RELAT_1:def 18;
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then A: dom p c= dom the Object-Kind of S by B, C, XBOOLE_1:1;
for x being set st x in dom p holds
p . x in the Object-Kind of S . x

proof

let x be set ; :: thesis: ( x in dom p implies p . x in the Object-Kind of S . x )
assume Z: x in dom p ; :: thesis: p . x in the Object-Kind of S . x
then reconsider x = x as Instruction-Location of S by C, AMI_1:def 4;
p . x in the Instructions of S by Z, PARTFUN1:27;
then p . x in ObjectKind x by AMI_1:def 14;
hence p . x in the Object-Kind of S . x ; :: thesis: verum

end;

then reconsider p = p as FinPartState of S by A, CARD_3:def 9;
dom p c= NAT by RELAT_1:def 18;
hence p is preProgram of S by RELAT_1:def 18; :: thesis: verum