let C1, C2 be Category; :: thesis: for F being Functor of C1,C2
for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
let F be Functor of C1,C2; :: thesis: for a, b being Object of C1 holds (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
let a, b be Object of C1; :: thesis: (Upsilon F) . (homsym (a,b)) = homsym ((F . a),(F . b))
A1: dom (Obj F) = the carrier of C1 by FUNCT_2:def 1;
thus (Upsilon F) . (homsym (a,b)) = [0,((Obj F) * ((homsym (a,b)) `2))] by Def13
.= [0,((Obj F) * <*a,b*>)] by MCART_1:7
.= [0,<*((Obj F) . a),((Obj F) . b)*>] by A1, FINSEQ_2:125
.= [0,<*(F . a),((Obj F) . b)*>] by CAT_1:def 17
.= homsym ((F . a),(F . b)) by CAT_1:def 17 ; :: thesis: verum