let C1, C2 be Category; :: thesis: for F being Functor of C1,C2

for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

let F be Functor of C1,C2; :: thesis: for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

let a be Object of C1; :: thesis: (Psi F) . (idsym a) = idsym (F . a)

A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def 1;

( (idsym a) `1 = 1 & (idsym a) `2 = <*a*> ) ;

hence (Psi F) . (idsym a) = [1,((Obj F) * <*a*>)] by Def12

.= [1,<*((Obj F) . a)*>] by A1, Lm4

.= idsym (F . a) ;

:: thesis: verum

for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

let F be Functor of C1,C2; :: thesis: for a being Object of C1 holds (Psi F) . (idsym a) = idsym (F . a)

let a be Object of C1; :: thesis: (Psi F) . (idsym a) = idsym (F . a)

A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def 1;

( (idsym a) `1 = 1 & (idsym a) `2 = <*a*> ) ;

hence (Psi F) . (idsym a) = [1,((Obj F) * <*a*>)] by Def12

.= [1,<*((Obj F) . a)*>] by A1, Lm4

.= idsym (F . a) ;

:: thesis: verum