let C be non empty non void with_triple-like_morphisms CatStr ; :: thesis: for f being Morphism of C holds
( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] )
let f be Morphism of C; :: thesis: ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] )
ex x being set st f = [[(dom f),(cod f)],x] by Def1;
hence ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2)] ) by MCART_1:85; :: thesis: verum