let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program steady-programmed AMI-Struct of N
for i being Instruction of S
for s being State of S holds ProgramPart (Exec (i,s)) = ProgramPart s
let S be non empty stored-program steady-programmed AMI-Struct of N; :: thesis: for i being Instruction of S
for s being State of S holds ProgramPart (Exec (i,s)) = ProgramPart s
let i be Instruction of S; :: thesis: for s being State of S holds ProgramPart (Exec (i,s)) = ProgramPart s
let s be State of S; :: thesis: ProgramPart (Exec (i,s)) = ProgramPart s
A1: NAT c= the carrier of S by COMPOS_1:def 2;
A2: for x being set st x in NAT holds
((Exec (i,s)) | NAT) . x = (s | NAT) . x

proof

let x be set ; :: thesis: ( x in NAT implies ((Exec (i,s)) | NAT) . x = (s | NAT) . x )
assume x in NAT ; :: thesis: ((Exec (i,s)) | NAT) . x = (s | NAT) . x
then reconsider l = x as Element of NAT ;
thus ((Exec (i,s)) | NAT) . x = (Exec (i,s)) . l by FUNCT_1:72
.= s . l by Def13
.= (s | NAT) . x by FUNCT_1:72 ; :: thesis: verum

end;

A4: dom (ProgramPart s) = NAT by COMPOS_1:34;
dom (Exec (i,s)) = the carrier of S by PARTFUN1:def 4;
then dom ((Exec (i,s)) | NAT) = NAT by A1, RELAT_1:91;
hence ProgramPart (Exec (i,s)) = ProgramPart s by A4, A2, FUNCT_1:9; :: thesis: verum