let s1, s2 be State of SCM+FSA ; :: thesis: ( ( for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )
A1: ( ( for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l ) implies for l being set st l in NAT holds
s1 . l = s2 . l )

proof

assume A2: for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l ; :: thesis: for l being set st l in NAT holds
s1 . l = s2 . l
let l be set ; :: thesis: ( l in NAT implies s1 . l = s2 . l )
assume l in NAT ; :: thesis: s1 . l = s2 . l
then reconsider l = l as Instruction-Location of SCM+FSA by AMI_1:def 4;
s1 . l = s2 . l by A2;
hence s1 . l = s2 . l ; :: thesis: verum

end;

A3: ( ( for l being set st l in NAT holds
s1 . l = s2 . l ) implies for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l )

proof

assume A4: for l being set st l in NAT holds
s1 . l = s2 . l ; :: thesis: for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l
let l be Instruction-Location of SCM+FSA ; :: thesis: s1 . l = s2 . l
l in NAT by AMI_1:def 4;
hence s1 . l = s2 . l by A4; :: thesis: verum

end;

( NAT c= dom s1 & NAT c= dom s2 ) by AMI_1:114;
hence ( ( for l being Instruction-Location of SCM+FSA holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT ) by A1, A3, FUNCT_1:165; :: thesis: verum