let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for A being non empty stored-program AMI-Struct of IL,N
for s being State of A
for o being Object of A holds s . o in ObjectKind o
let IL be non empty set ; :: thesis: for A being non empty stored-program AMI-Struct of IL,N
for s being State of A
for o being Object of A holds s . o in ObjectKind o
let A be non empty stored-program AMI-Struct of IL,N; :: thesis: for s being State of A
for o being Object of A holds s . o in ObjectKind o
let s be State of A; :: thesis: for o being Object of A holds s . o in ObjectKind o
let o be Object of A; :: thesis: s . o in ObjectKind o
dom the Object-Kind of A = the carrier of A by FUNCT_2:def 1;
hence s . o in ObjectKind o by CARD_3:18; :: thesis: verum