let x1, x2 be set ; :: thesis: for C being Category
for p1, p2, f being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) * f = x1,x2 --> (p1 * f),(p2 * f)
let C be Category; :: thesis: for p1, p2, f being Morphism of C st x1 <> x2 holds
(x1,x2 --> p1,p2) * f = x1,x2 --> (p1 * f),(p2 * f)
let p1, p2, f be Morphism of C; :: thesis: ( x1 <> x2 implies (x1,x2 --> p1,p2) * f = x1,x2 --> (p1 * f),(p2 * f) )
assume A1: x1 <> x2 ; :: thesis: (x1,x2 --> p1,p2) * f = x1,x2 --> (p1 * f),(p2 * f)
set F = x1,x2 --> p1,p2;
set F' = x1,x2 --> (p1 * f),(p2 * f);

now

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

end;

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