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

now

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

end;

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