reconsider A = the Execution of S . i as Function of (product the Object-Kind of S),(product the Object-Kind of S) by FUNCT_2:121;
reconsider s = s as Element of product the Object-Kind of S by PBOOLE:155;
A . s in product the Object-Kind of S ;
hence ( ( the Execution of S . i) . s is Function-like & ( the Execution of S . i) . s is Relation-like ) ; :: thesis: verum