theorem :: ALTCAT_1:15

for C being non empty AltCatStr
for a1, a2, a3 being Object of C holds the Comp of C . (a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^> ;