let C be Category; :: thesis: for a being Object of C

for f being Morphism of C holds

( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

let a be Object of C; :: thesis: for f being Morphism of C holds

( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

let f be Morphism of C; :: thesis: ( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

A1: cod (id a) = a ;

for f being Morphism of C holds

( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

let a be Object of C; :: thesis: for f being Morphism of C holds

( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

let f be Morphism of C; :: thesis: ( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

A1: cod (id a) = a ;

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

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

hence
hom ((id a),f) = hom (a,f)
; :: thesis: hom (f,(id a)) = hom (f,a)(hom ((id a),f)) . x = (hom (a,f)) . x ) )

Hom ((dom f),(cod f)) <> {}
by CAT_1:2;

then ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

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

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

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

assume A2: x in Hom (a,(dom f)) ; :: thesis: (hom ((id a),f)) . x = (hom (a,f)) . x

then reconsider g = x as Morphism of C ;

A3: dom g = a by A2, CAT_1:1;

A4: cod g = dom f by A2, CAT_1:1;

thus (hom ((id a),f)) . x = (f (*) g) (*) (id a) by A2, Def22

.= f (*) (g (*) (id a)) by A1, A3, A4, CAT_1:18

.= f (*) g by A3, CAT_1:22

.= (hom (a,f)) . x by A2, Def18 ; :: thesis: verum

end;then ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) by CAT_1:24;

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

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

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

assume A2: x in Hom (a,(dom f)) ; :: thesis: (hom ((id a),f)) . x = (hom (a,f)) . x

then reconsider g = x as Morphism of C ;

A3: dom g = a by A2, CAT_1:1;

A4: cod g = dom f by A2, CAT_1:1;

thus (hom ((id a),f)) . x = (f (*) g) (*) (id a) by A2, Def22

.= f (*) (g (*) (id a)) by A1, A3, A4, CAT_1:18

.= f (*) g by A3, CAT_1:22

.= (hom (a,f)) . x by A2, Def18 ; :: thesis: verum

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

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

hence
hom (f,(id a)) = hom (f,a)
; :: thesis: verum(hom (f,(id a))) . x = (hom (f,a)) . x ) )

Hom ((dom f),(cod f)) <> {}
by CAT_1:2;

then ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;

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

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

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

assume A5: x in Hom ((cod f),a) ; :: thesis: (hom (f,(id a))) . x = (hom (f,a)) . x

then reconsider g = x as Morphism of C ;

A6: cod g = a by A5, CAT_1:1;

thus (hom (f,(id a))) . x = ((id a) (*) g) (*) f by A5, Def22

.= g (*) f by A6, CAT_1:21

.= (hom (f,a)) . x by A5, Def19 ; :: thesis: verum

end;then ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;

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

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

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

assume A5: x in Hom ((cod f),a) ; :: thesis: (hom (f,(id a))) . x = (hom (f,a)) . x

then reconsider g = x as Morphism of C ;

A6: cod g = a by A5, CAT_1:1;

thus (hom (f,(id a))) . x = ((id a) (*) g) (*) f by A5, Def22

.= g (*) f by A6, CAT_1:21

.= (hom (f,a)) . x by A5, Def19 ; :: thesis: verum