let x1, x2 be set ; 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; 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; ( 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
; ((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))
now for x being set st x in {x1,x2} holds
(((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 (*) q1),(p2 (*) q2))) /. xlet x be
set ;
( 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}
;
(((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 (*) q1),(p2 (*) q2))) /. xthen
(
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, Th3;
hence
(((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2))) /. x = ((x1,x2) --> ((p1 (*) q1),(p2 (*) q2))) /. x
by A2, Def7;
verum end;
hence
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))
by Th1; verum