let x1, x2 be set ; 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; 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; 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 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 for x being set st x in {x1,x2} holds
(cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. xlet x be
set ;
( x in {x1,x2} implies (cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. x )assume A5:
x in {x1,x2}
;
(cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. xthen A6:
x in dom ((x1,x2) --> (p1,p2))
by FUNCT_4:62;
now ( ( 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 A3, A6, FUNCT_4:12;
case A7:
(
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 )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) --> ((cod p1),(cod p2))) . x = (x1 .--> (cod p1)) . x
by A1, A2, A7, FUNCT_4:11;
then
((x1,x2) --> ((cod p1),(cod p2))) . x = cod p1
by A4, A7, FUNCOP_1:7;
hence
(
((x1,x2) --> (p1,p2)) /. x = p1 &
((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p1 )
by A5, A8, FUNCT_2:def 13;
verum end; case A9:
x in dom (x2 .--> p2)
;
( ((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 A3, FUNCT_4:13;
then A10:
((x1,x2) --> (p1,p2)) . x = p2
by A1, A9, FUNCOP_1:7;
((x1,x2) --> ((cod p1),(cod p2))) . x = (x2 .--> (cod p2)) . x
by A1, A2, A9, FUNCT_4:13;
then
((x1,x2) --> ((cod p1),(cod p2))) . x = cod p2
by A1, A9, FUNCOP_1:7;
hence
(
((x1,x2) --> (p1,p2)) /. x = p2 &
((x1,x2) --> ((cod p1),(cod p2))) /. x = cod p2 )
by A5, A10, FUNCT_2:def 13;
verum end; end; end; hence
(cods ((x1,x2) --> (p1,p2))) /. x = ((x1,x2) --> ((cod p1),(cod p2))) /. x
by A5, Def2;
verum end;
hence
cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))
by Th1; verum