consider f being Function such that
A1: ( the Execution of S . I = f & dom f = product the Object-Kind of S ) and
A2: rng f c= product the Object-Kind of S by FUNCT_2:def 2;
reconsider s = s as Element of product the Object-Kind of S by PBOOLE:155;
(the Execution of S . I) . s in rng f by A1, FUNCT_1:def 5;
hence (the Execution of S . I) . s is State of S by A2; :: thesis: verum