let x1, x2 be set ; :: thesis: for C being Category
for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
x1,x2 --> p1,p2 is Projections_family of a,{x1,x2}
let C be Category; :: thesis: for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
x1,x2 --> p1,p2 is Projections_family of a,{x1,x2}
let a be Object of C; :: thesis: for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
x1,x2 --> p1,p2 is Projections_family of a,{x1,x2}
let p1, p2 be Morphism of C; :: thesis: ( dom p1 = a & dom p2 = a implies x1,x2 --> p1,p2 is Projections_family of a,{x1,x2} )
assume A1: ( dom p1 = a & dom p2 = a ) ; :: thesis: x1,x2 --> p1,p2 is Projections_family of a,{x1,x2}
doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2) by Th10
.= {x1,x2} --> a by A1, FUNCT_4:68 ;
hence x1,x2 --> p1,p2 is Projections_family of a,{x1,x2} by Def14; :: thesis: verum