let C be Category; :: thesis: for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))

let a, c be Object of C; :: thesis: hom (a,(id c)) = id (Hom (a,c))

set A = Hom (a,c);

let a, c be Object of C; :: thesis: hom (a,(id c)) = id (Hom (a,c))

set A = Hom (a,c);

now :: thesis: ( dom (hom (a,(id c))) = Hom (a,c) & ( for x being object st x in Hom (a,c) holds

(hom (a,(id c))) . x = x ) )

hence
hom (a,(id c)) = id (Hom (a,c))
by FUNCT_1:17; :: thesis: verum(hom (a,(id c))) . x = x ) )

( Hom (a,c) = {} implies Hom (a,c) = {} )
;

hence dom (hom (a,(id c))) = Hom (a,c) by FUNCT_2:def 1; :: thesis: for x being object st x in Hom (a,c) holds

(hom (a,(id c))) . x = x

let x be object ; :: thesis: ( x in Hom (a,c) implies (hom (a,(id c))) . x = x )

assume A1: x in Hom (a,c) ; :: thesis: (hom (a,(id c))) . x = x

then reconsider g = x as Morphism of C ;

A2: cod g = c by A1, CAT_1:1;

thus (hom (a,(id c))) . x = (id c) (*) g by A1, Def18

.= x by A2, CAT_1:21 ; :: thesis: verum

end;hence dom (hom (a,(id c))) = Hom (a,c) by FUNCT_2:def 1; :: thesis: for x being object st x in Hom (a,c) holds

(hom (a,(id c))) . x = x

let x be object ; :: thesis: ( x in Hom (a,c) implies (hom (a,(id c))) . x = x )

assume A1: x in Hom (a,c) ; :: thesis: (hom (a,(id c))) . x = x

then reconsider g = x as Morphism of C ;

A2: cod g = c by A1, CAT_1:1;

thus (hom (a,(id c))) . x = (id c) (*) g by A1, Def18

.= x by A2, CAT_1:21 ; :: thesis: verum