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

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