consider A being set such that
CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},(2 -tuples_on A):] by Def6;
s `2 in 2 -tuples_on A by A1, MCART_1:10;
hence ( s `2 is Relation-like & s `2 is Function-like ) ; :: thesis: verum