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