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 Def4;
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