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