let x1, x2 be set ; :: thesis: for C being Category

for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let C be Category; :: thesis: for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let c be Object of C; :: thesis: for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let p1, p2 be Morphism of C; :: thesis: ( cod p1 = c & cod p2 = c implies (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2} )

assume A1: ( cod p1 = c & cod p2 = c ) ; :: thesis: (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2)) by Th7

.= {x1,x2} --> c by A1, FUNCT_4:65 ;

hence (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2} by Def16; :: thesis: verum

for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let C be Category; :: thesis: for c being Object of C

for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let c be Object of C; :: thesis: for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds

(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

let p1, p2 be Morphism of C; :: thesis: ( cod p1 = c & cod p2 = c implies (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2} )

assume A1: ( cod p1 = c & cod p2 = c ) ; :: thesis: (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}

cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2)) by Th7

.= {x1,x2} --> c by A1, FUNCT_4:65 ;

hence (x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2} by Def16; :: thesis: verum