let C be non empty transitive AltCatStr ; :: thesis: 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^> )
let a1, a2, a3 be Object of C; :: thesis: ( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> )
( not <^a1,a3^> = {} or <^a1,a2^> = {} or <^a2,a3^> = {} ) by Def2;
then ( <^a1,a3^> = {} implies [:<^a2,a3^>,<^a1,a2^>:] = {} ) ;
hence ( dom ( the Comp of C . (a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng ( the Comp of C . (a1,a2,a3)) c= <^a1,a3^> ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum