reconsider A = the Execution of S . i as Function of (product (the_Values_of S)),(product (the_Values_of S)) by FUNCT_2:66;
reconsider s = s as Element of product (the_Values_of S) by CARD_3:107;
A . s in product (the_Values_of S) ;
hence ( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like ) ; :: thesis: verum