let x1, x2 be set ; :: thesis: for C being Category
for p1, p2 being Morphism of C holds doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2)
let C be Category; :: thesis: for p1, p2 being Morphism of C holds doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2)
let p1, p2 be Morphism of C; :: thesis: doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2)
set F = x1,x2 --> p1,p2;
set f = x1 .--> p1;
set g = x2 .--> p2;
set F9 = x1,x2 --> (dom p1),(dom p2);
set f9 = x1 .--> (dom p1);
set g9 = x2 .--> (dom p2);
A1: dom (x2 .--> p2) = {x2} by FUNCOP_1:19;
A2: ( dom (x2 .--> (dom p2)) = {x2} & x1,x2 --> (dom p1),(dom p2) = (x1 .--> (dom p1)) +* (x2 .--> (dom p2)) ) by FUNCOP_1:19, FUNCT_4:def 4;
A3: x1,x2 --> p1,p2 = (x1 .--> p1) +* (x2 .--> p2) by FUNCT_4:def 4;
A4: dom (x1 .--> p1) = {x1} by FUNCOP_1:19;

now

let x be set ; :: thesis: ( x in {x1,x2} implies (doms (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (dom p1),(dom p2)) /. x )
assume A5: x in {x1,x2} ; :: thesis: (doms (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (dom p1),(dom p2)) /. x
then A6: x in dom (x1,x2 --> p1,p2) by FUNCT_4:65;

now

per cases ( ( x in dom (x1 .--> p1) & not x in dom (x2 .--> p2) ) or x in dom (x2 .--> p2) ) by A3, A6, FUNCT_4:13;

case A7: ( x in dom (x1 .--> p1) & not x in dom (x2 .--> p2) ) ; :: thesis: ( (x1,x2 --> p1,p2) /. x = p1 & (x1,x2 --> (dom p1),(dom p2)) /. x = dom p1 )

then (x1,x2 --> p1,p2) . x = (x1 .--> p1) . x by A3, FUNCT_4:12;
then A8: (x1,x2 --> p1,p2) . x = p1 by A4, A7, FUNCOP_1:13;
(x1,x2 --> (dom p1),(dom p2)) . x = (x1 .--> (dom p1)) . x by A1, A2, A7, FUNCT_4:12;
then (x1,x2 --> (dom p1),(dom p2)) . x = dom p1 by A4, A7, FUNCOP_1:13;
hence ( (x1,x2 --> p1,p2) /. x = p1 & (x1,x2 --> (dom p1),(dom p2)) /. x = dom p1 ) by A5, A8, FUNCT_2:def 14; :: thesis: verum

end;

case A9: x in dom (x2 .--> p2) ; :: thesis: ( (x1,x2 --> p1,p2) /. x = p2 & (x1,x2 --> (dom p1),(dom p2)) /. x = dom p2 )

then (x1,x2 --> p1,p2) . x = (x2 .--> p2) . x by A3, FUNCT_4:14;
then A10: (x1,x2 --> p1,p2) . x = p2 by A1, A9, FUNCOP_1:13;
(x1,x2 --> (dom p1),(dom p2)) . x = (x2 .--> (dom p2)) . x by A1, A2, A9, FUNCT_4:14;
then (x1,x2 --> (dom p1),(dom p2)) . x = dom p2 by A1, A9, FUNCOP_1:13;
hence ( (x1,x2 --> p1,p2) /. x = p2 & (x1,x2 --> (dom p1),(dom p2)) /. x = dom p2 ) by A5, A10, FUNCT_2:def 14; :: thesis: verum

end;

end;

end;

hence (doms (x1,x2 --> p1,p2)) /. x = (x1,x2 --> (dom p1),(dom p2)) /. x by A5, Def3; :: thesis: verum

end;

hence doms (x1,x2 --> p1,p2) = x1,x2 --> (dom p1),(dom p2) by Th1; :: thesis: verum