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;
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