let A be category; :: thesis: for a, b being object of A st <^a,b^> <> {} holds
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: ( <^a,b^> <> {} implies 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 )
assume <^a,b^> <> {} ; :: 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
( F1 in Funcs ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) & F2 in Funcs ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) ) by A1, A2, Def12;
then A4: ( dom F1 = (Concretized A) -carrier_of a & dom F2 = (Concretized A) -carrier_of a ) by FUNCT_2:169;
consider fa, fb being object of A, f being Morphism of fa,fb such that
A5: ( fa = a & fb = b & <^fa,fb^> <> {} ) and
A6: 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
A7: ( ga = a & gb = b & <^ga,gb^> <> {} ) and
A8: 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 A5, A7;
( F1 . [(idm a),[a,a]] = [(f * (idm a)),[a,b]] & f * (idm a) = f & g * (idm a) = g & F2 . [(idm a),[a,a]] = [(g * (idm a)),[a,b]] ) by A5, A6, A7, A8, ALTCAT_1:def 19;
then A9: f = g by A3, ZFMISC_1:33;

now

let x be set ; :: 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
A10: ( <^bb,a^> <> {} & x = [ff,[bb,a]] ) by Th45;
thus F1 . x = [(f * ff),[bb,b]] by A5, A6, A10
.= F2 . x by A7, A8, A9, A10 ; :: thesis: verum

end;

hence F1 = F2 by A4, FUNCT_1:9; :: thesis: verum