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:13;
A2: ( dom (x2 .--> (dom p2)) = {x2} & (x1,x2) --> ((dom p1),(dom p2)) = (x1 .--> (dom p1)) +* (x2 .--> (dom p2)) ) by FUNCOP_1:13, 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:13;

now :: thesis: for x being set st x in {x1,x2} holds
(doms ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((dom p1),(dom p2))) /. x

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:62;

now :: thesis: ( ( x in dom (x1 .--> p1) & not x in dom (x2 .--> p2) & ((x1,x2) --> (p1,p2)) /. x = p1 & ((x1,x2) --> ((dom p1),(dom p2))) /. x = dom p1 ) or ( x in dom (x2 .--> p2) & ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> ((dom p1),(dom p2))) /. x = dom p2 ) )

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

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:11;
then A8: ((x1,x2) --> (p1,p2)) . x = p1 by A4, A7, FUNCOP_1:7;
((x1,x2) --> ((dom p1),(dom p2))) . x = (x1 .--> (dom p1)) . x by A1, A2, A7, FUNCT_4:11;
then ((x1,x2) --> ((dom p1),(dom p2))) . x = dom p1 by A4, A7, FUNCOP_1:7;
hence ( ((x1,x2) --> (p1,p2)) /. x = p1 & ((x1,x2) --> ((dom p1),(dom p2))) /. x = dom p1 ) by A5, A8, FUNCT_2:def 13; :: 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:13;
then A10: ((x1,x2) --> (p1,p2)) . x = p2 by A1, A9, FUNCOP_1:7;
((x1,x2) --> ((dom p1),(dom p2))) . x = (x2 .--> (dom p2)) . x by A1, A2, A9, FUNCT_4:13;
then ((x1,x2) --> ((dom p1),(dom p2))) . x = dom p2 by A1, A9, FUNCOP_1:7;
hence ( ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> ((dom p1),(dom p2))) /. x = dom p2 ) by A5, A10, FUNCT_2:def 13; :: thesis: verum

end;

end;

end;

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

end;

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