A1: NAT c= the carrier of S by AMI_1:def 3;
A2: 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 A3: dom p c= dom the Object-Kind of S by A1, A2, 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 A4: x in dom p ; :: thesis: p . x in the Object-Kind of S . x
then reconsider x = x as Instruction-Location of S by A2, AMI_1:def 4;
p . x in the Instructions of S by A4, 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 by A3, CARD_3:def 9;
dom p c= NAT by RELAT_1:def 18;
hence p is preProgram of S ; :: thesis: verum