let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s1, s2 being State of S holds
( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s1, s2 being State of S holds
( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT )
let s1, s2 be State of S; :: 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 LmL;
hence ( ( for l being Element of NAT holds s1 . l = s2 . l ) iff s1 | NAT = s2 | NAT ) by A1, FUNCT_1:165; :: thesis: verum