let C be Categorial Category; :: thesis: for f being Morphism of C holds
( dom f = f `11 & cod f = f `12 )
let f be Morphism of C; :: thesis: ( dom f = f `11 & cod f = f `12 )
reconsider A = dom f, B = cod f as Category by Th12;
ex F being Functor of A,B st f = [[A,B],F] by Def6;
hence ( dom f = f `11 & cod f = f `12 ) by MCART_1:85; :: thesis: verum