let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite COM-Struct of N
for I being Element of the Instructions of S
for s being State of S holds s +* (NAT --> I) is State of S
let S be non empty stored-program definite COM-Struct of N; :: thesis: for I being Element of the Instructions of S
for s being State of S holds s +* (NAT --> I) is State of S
let I be Element of the Instructions of S; :: thesis: for s being State of S holds s +* (NAT --> I) is State of S
let s be State of S; :: thesis: s +* (NAT --> I) is State of S
set f = NAT --> I;
set Ok = the Object-Kind of S;
A1: ( dom (NAT --> I) = NAT & NAT c= the carrier of S ) by Def3, FUNCOP_1:19;
NAT --> I is PartState of S by A1, RELAT_1:def 18;
hence s +* (NAT --> I) is State of S ; :: thesis: verum