let s1, s2 be State of SCMPDS ; :: thesis: ( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )
A1: ( ( for l being Element of NAT holds s1 . l = s2 . l ) implies for l being set st l in NAT holds
s1 . l = s2 . l ) ;
( NAT c= dom s1 & NAT c= dom s2 ) by COMPOS_1:21;
hence ( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT ) by A1, FUNCT_1:165; :: thesis: verum