let N be with_zero set ; :: thesis: for A being non empty with_non-empty_values Mem-Struct over N
for s being State of A
for o being Object of A holds s . o in Values o
let A be non empty with_non-empty_values Mem-Struct over N; :: thesis: for s being State of A
for o being Object of A holds s . o in Values o
let s be State of A; :: thesis: for o being Object of A holds s . o in Values o
let o be Object of A; :: thesis: s . o in Values o
dom s = the carrier of A by PARTFUN1:def 2;
hence s . o in Values o by FUNCT_1:def 14; :: thesis: verum