let x1, x2 be set ; :: thesis: for C being Category
for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 * q1),(p2 * q2))
let C be Category; :: thesis: for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 * q1),(p2 * q2))
let p1, p2, q1, q2 be Morphism of C; :: thesis: ( x1 <> x2 implies ((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 * q1),(p2 * q2)) )
set F1 = (x1,x2) --> (p1,p2);
set F2 = (x1,x2) --> (q1,q2);
set G = (x1,x2) --> ((p1 * q1),(p2 * q2));
assume A1: x1 <> x2 ; :: thesis: ((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 * q1),(p2 * q2))

now

let x be set ; :: thesis: ( x in {x1,x2} implies (((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 * q1),(p2 * q2))) /. x )
assume A2: x in {x1,x2} ; :: thesis: (((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 * q1),(p2 * q2))) /. x
then ( x = x1 or x = x2 ) by TARSKI:def 2;
then ( ( ((x1,x2) --> (p1,p2)) /. x = p1 & ((x1,x2) --> (q1,q2)) /. x = q1 & ((x1,x2) --> ((p1 * q1),(p2 * q2))) /. x = p1 * q1 ) or ( ((x1,x2) --> (p1,p2)) /. x = p2 & ((x1,x2) --> (q1,q2)) /. x = q2 & ((x1,x2) --> ((p1 * q1),(p2 * q2))) /. x = p2 * q2 ) ) by A1, Th7;
hence (((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 * q1),(p2 * q2))) /. x by A2, Def9; :: thesis: verum

end;

hence ((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 * q1),(p2 * q2)) by Th1; :: thesis: verum