set M = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;
{ f where f is Morphism of C : ( dom f = a & cod f = b ) } c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Morphism of C : ( dom f = a & cod f = b ) } or x in the carrier' of C )
assume x in { f where f is Morphism of C : ( dom f = a & cod f = b ) } ; :: thesis: x in the carrier' of C
then ex f being Morphism of C st
( x = f & dom f = a & cod f = b ) ;
hence x in the carrier' of C ; :: thesis: verum
end;
hence { f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C ; :: thesis: verum