let i be Instruction of SCM ; :: thesis: for s being State of SCM holds (Exec i,s) | NAT = s | NAT
let s be State of SCM ; :: thesis: (Exec i,s) | NAT = s | NAT
A1: 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 AMI_1:def 13
.= (s | NAT ) . x by FUNCT_1:72 ; :: thesis: verum

end;

dom s = the carrier of SCM by PARTFUN1:def 4;
then A3: dom (s | NAT ) = NAT by RELAT_1:91;
dom (Exec i,s) = the carrier of SCM by PARTFUN1:def 4;
then dom ((Exec i,s) | NAT ) = NAT by RELAT_1:91;
hence (Exec i,s) | NAT = s | NAT by A3, A1, FUNCT_1:9; :: thesis: verum