let x1, x2 be set ; :: thesis: for C being Category
for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))

let C be Category; :: thesis: for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))
let p1, p2 be Morphism of C; :: thesis: cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))
set F = (x1,x2) --> (p1,p2);
set f = x1 .--> p1;
set g = x2 .--> p2;
set F9 = (x1,x2) --> ((cod p1),(cod p2));
set f9 = x1 .--> (cod p1);
set g9 = x2 .--> (cod p2);
A1: dom (x2 .--> p2) = {x2} by FUNCOP_1:13;
A2: ( dom (x2 .--> (cod p2)) = {x2} & (x1,x2) --> ((cod p1),(cod p2)) = (x1 .--> (cod p1)) +* (x2 .--> (cod p2)) ) by ;
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
(cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. x
let x be set ; :: thesis: ( x in {x1,x2} implies (cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. x )
assume A5: x in {x1,x2} ; :: thesis: (cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod 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) --> ((cod p1),(cod p2))) /. x = cod p1 ) or ( x in dom (x2 .--> p2) & ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p2 ) )
per cases ( ( x in dom (x1 .--> p1) & not x in dom (x2 .--> p2) ) or x in dom (x2 .--> p2) ) by ;
case A7: ( x in dom (x1 .--> p1) & not x in dom (x2 .--> p2) ) ; :: thesis: ( ((x1,x2) --> (p1,p2)) /. x = p1 & ((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p1 )
then ((x1,x2) --> (p1,p2)) . x = (x1 .--> p1) . x by ;
then A8: ((x1,x2) --> (p1,p2)) . x = p1 by ;
((x1,x2) --> ((cod p1),(cod p2))) . x = (x1 .--> (cod p1)) . x by ;
then ((x1,x2) --> ((cod p1),(cod p2))) . x = cod p1 by ;
hence ( ((x1,x2) --> (p1,p2)) /. x = p1 & ((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p1 ) by ; :: thesis: verum
end;
case A9: x in dom (x2 .--> p2) ; :: thesis: ( ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p2 )
then ((x1,x2) --> (p1,p2)) . x = (x2 .--> p2) . x by ;
then A10: ((x1,x2) --> (p1,p2)) . x = p2 by ;
((x1,x2) --> ((cod p1),(cod p2))) . x = (x2 .--> (cod p2)) . x by ;
then ((x1,x2) --> ((cod p1),(cod p2))) . x = cod p2 by ;
hence ( ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p2 ) by ; :: thesis: verum
end;
end;
end;
hence (cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. x by ; :: thesis: verum
end;
hence cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2)) by Th1; :: thesis: verum