consider A being set such that
CatSign A is Subsignature of S and
A1: the carrier of S = [:{0},(2 -tuples_on A):] by Def4;
s `2 in 2 -tuples_on A by A1, MCART_1:10;
hence for b<sub>1</sub> being set st b<sub>1</sub> = s `2 holds
( b₁ is Relation-like & b₁ is Function-like ) ; :: thesis: verum