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*> ) by MCART_1:7;
hence (Psi F) . (compsym a,b,c) = [2,((Obj F) * <*a,b,c*>)] by Def14
.= [2,<*((Obj F) . a),((Obj F) . b),((Obj F) . c)*>] by A1, FINSEQ_2:146
.= [2,<*(F . a),((Obj F) . b),((Obj F) . c)*>] by CAT_1:def 20
.= [2,<*(F . a),(F . b),((Obj F) . c)*>] by CAT_1:def 20
.= compsym (F . a),(F . b),(F . c) by CAT_1:def 20 ;
:: thesis: verum