theorem :: ALTCAT_1:17

for C being non empty transitive AltCatStr
for a1, a2, a3 being Object of C holds
( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )