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:7, MCART_1:89; :: thesis: verum