let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program definite AMI-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 AMI-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 AMI_1:def 3, FUNCOP_1:19;
for x being set st x in dom (NAT --> I) holds
(NAT --> I) . x in the Object-Kind of S . x

proof

let x be set ; :: thesis: ( x in dom (NAT --> I) implies (NAT --> I) . x in the Object-Kind of S . x )
assume A3: x in dom (NAT --> I) ; :: thesis: (NAT --> I) . x in the Object-Kind of S . x
then A4: (NAT --> I) . x = I by FUNCOP_1:13;
reconsider x = x as Element of NAT by A3;
the Object-Kind of S . x = the Instructions of S by AMI_1:def 14;
hence (NAT --> I) . x in the Object-Kind of S . x by A4; :: thesis: verum

end;

then NAT --> I is the Object-Kind of S -compatible by FUNCT_1:def 20;
then NAT --> I is PartState of S by A1, RELAT_1:def 18;
hence s +* (NAT --> I) is State of S ; :: thesis: verum