let A be category; :: thesis: 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; :: thesis: 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; :: thesis: ( 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]] ; :: thesis: 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, XTUPLE_0:1;

now :: thesis: for x being object st x in (Concretized A) -carrier_of a holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in (Concretized A) -carrier_of a implies F1 . x = F2 . x )
assume x in (Concretized A) -carrier_of a ; :: thesis: F1 . x = F2 . x
then consider bb being Object of A, ff being Morphism of bb,a such that
A19: <^bb,a^> <> {} and
A20: x = [ff,[bb,a]] by Th43;
thus F1 . x = [(f * ff),[bb,b]] by A8, A9, A11, A19, A20
.= F2 . x by A12, A13, A14, A18, A19, A20 ; :: thesis: verum

end;

hence F1 = F2 by A6, A7; :: thesis: verum