let C be Cartesian_category; for a, b, c being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let a, b, c be Object of C; for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let f be Morphism of c,a; for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
<:f,g:> = (f [x] g) * (Delta c)
let g be Morphism of c,b; ( Hom (c,a) <> {} & Hom (c,b) <> {} implies <:f,g:> = (f [x] g) * (Delta c) )
assume that
A1:
Hom (c,a) <> {}
and
A2:
Hom (c,b) <> {}
; <:f,g:> = (f [x] g) * (Delta c)
Hom (c,c) <> {}
;
hence (f [x] g) * (Delta c) =
<:(f * (id c)),(g * (id c)):>
by A1, A2, Th41
.=
<:f,(g * (id c)):>
by A1, CAT_1:29
.=
<:f,g:>
by A2, CAT_1:29
;
verum