let C1, C2 be Category; :: thesis: for F being Functor of C1,C2
for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))
let F be Functor of C1,C2; :: thesis: for a, b, c being Object of C1 holds (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))
let a, b, c be Object of C1; :: thesis: (Psi F) . (compsym (a,b,c)) = compsym ((F . a),(F . b),(F . c))
A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def 1;
( (compsym (a,b,c)) `1 = 2 & (compsym (a,b,c)) `2 = <*a,b,c*> ) ;
hence (Psi F) . (compsym (a,b,c)) = [2,((Obj F) * <*a,b,c*>)] by Def12
.= [2,<*((Obj F) . a),((Obj F) . b),((Obj F) . c)*>] by A1, FINSEQ_2:126
.= [2,<*(F . a),((Obj F) . b),((Obj F) . c)*>]
.= [2,<*(F . a),(F . b),((Obj F) . c)*>]
.= compsym ((F . a),(F . b),(F . c)) ;
:: thesis: verum