let A be category; for a, b being object of A
for F1, F2 being Function st F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds
F1 = F2
let a, b be object of A; for F1, F2 being Function st F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] holds
F1 = F2
set B = Concretized A;
let F1, F2 be Function; ( F1 in the Arrows of (Concretized A) . (a,b) & F2 in the Arrows of (Concretized A) . (a,b) & F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]] implies F1 = F2 )
assume that
A1:
F1 in the Arrows of (Concretized A) . (a,b)
and
A2:
F2 in the Arrows of (Concretized A) . (a,b)
and
A3:
F1 . [(idm a),[a,a]] = F2 . [(idm a),[a,a]]
; F1 = F2
A4:
F1 in Funcs (((Concretized A) -carrier_of a),((Concretized A) -carrier_of b))
by A1, Def12;
A5:
F2 in Funcs (((Concretized A) -carrier_of a),((Concretized A) -carrier_of b))
by A2, Def12;
A6:
dom F1 = (Concretized A) -carrier_of a
by A4, FUNCT_2:92;
A7:
dom F2 = (Concretized A) -carrier_of a
by A5, FUNCT_2:92;
consider fa, fb being object of A, f being Morphism of fa,fb such that
A8:
fa = a
and
A9:
fb = b
and
A10:
<^fa,fb^> <> {}
and
A11:
for o being object of A st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds F1 . [h,[o,fa]] = [(f * h),[o,fb]]
by A1, Def12;
consider ga, gb being object of A, g being Morphism of ga,gb such that
A12:
ga = a
and
A13:
gb = b
and
<^ga,gb^> <> {}
and
A14:
for o being object of A st <^o,ga^> <> {} holds
for h being Morphism of o,ga holds F2 . [h,[o,ga]] = [(g * h),[o,gb]]
by A2, Def12;
reconsider f = f, g = g as Morphism of a,b by A8, A9, A12, A13;
A15:
F1 . [(idm a),[a,a]] = [(f * (idm a)),[a,b]]
by A8, A9, A11;
A16:
f * (idm a) = f
by A8, A9, A10, ALTCAT_1:def 17;
A17:
g * (idm a) = g
by A8, A9, A10, ALTCAT_1:def 17;
F2 . [(idm a),[a,a]] = [(g * (idm a)),[a,b]]
by A12, A13, A14;
then A18:
f = g
by A3, A15, A16, A17, ZFMISC_1:27;
now let x be
set ;
( x in (Concretized A) -carrier_of a implies F1 . x = F2 . x )assume
x in (Concretized A) -carrier_of a
;
F1 . x = F2 . xthen consider bb being
object of
A,
ff being
Morphism of
bb,
a such that A19:
<^bb,a^> <> {}
and A20:
x = [ff,[bb,a]]
by Th45;
thus F1 . x =
[(f * ff),[bb,b]]
by A8, A9, A11, A19, A20
.=
F2 . x
by A12, A13, A14, A18, A19, A20
;
verum end;
hence
F1 = F2
by A6, A7, FUNCT_1:2; verum