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 )] )
consider x being set such that
A1: f = [[(dom f),(cod f)],x] by Def1;
thus ( dom f = f `11 & cod f = f `12 & f = [[(dom f),(cod f)],(f `2 )] ) by A1, MCART_1:7, MCART_1:89; :: thesis: verum