let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program definite AMI-Struct of IL,N
for I being Element of the Instructions of S
for s being State of S holds s +* (IL --> I) is State of S
let IL be non empty set ; :: thesis: for S being non empty stored-program definite AMI-Struct of IL,N
for I being Element of the Instructions of S
for s being State of S holds s +* (IL --> I) is State of S
let S be non empty stored-program definite AMI-Struct of IL,N; :: thesis: for I being Element of the Instructions of S
for s being State of S holds s +* (IL --> I) is State of S
let I be Element of the Instructions of S; :: thesis: for s being State of S holds s +* (IL --> I) is State of S
let s be State of S; :: thesis: s +* (IL --> I) is State of S
set f = IL --> I;
set Ok = the Object-Kind of S;
A1: dom (IL --> I) = IL by FUNCOP_1:19;
A2: IL c= the carrier of S by AMI_1:def 3;
A3: dom s = the carrier of S by AMI_1:79;
then A4: dom the Object-Kind of S = dom s by FUNCT_2:def 1;
for x being set st x in dom (IL --> I) holds
(IL --> I) . x in the Object-Kind of S . x

proof

let x be set ; :: thesis: ( x in dom (IL --> I) implies (IL --> I) . x in the Object-Kind of S . x )
assume A5: x in dom (IL --> I) ; :: thesis: (IL --> I) . x in the Object-Kind of S . x
then A6: (IL --> I) . x = I by FUNCOP_1:13;
reconsider x = x as Instruction-Location of S by A5, AMI_1:def 4;
the Object-Kind of S . x = ObjectKind x
.= the Instructions of S by AMI_1:def 14 ;
hence (IL --> I) . x in the Object-Kind of S . x by A6; :: thesis: verum

end;

then IL --> I in sproduct the Object-Kind of S by A1, A2, A3, A4, CARD_3:def 9;
hence s +* (IL --> I) is State of S by CARD_3:69; :: thesis: verum