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

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