let N be 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 holds s +* (NAT --> I) is State of
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 holds s +* (NAT --> I) is State of
let I be Element of the Instructions of S; :: thesis: for s being State of holds s +* (NAT --> I) is State of
let s be State of ; :: thesis: s +* (NAT --> I) is State of
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;
A2: 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 Instruction-Location of S by A3, AMI_1:def 4;
the Object-Kind of S . x = ObjectKind 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;

A5: dom s = the carrier of S by AMI_1:79;
then dom the Object-Kind of S = dom s by FUNCT_2:def 1;
then NAT --> I in sproduct the Object-Kind of S by A1, A5, A2, CARD_3:def 9;
hence s +* (NAT --> I) is State of by CARD_3:69; :: thesis: verum