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