let f1, f2 be non-empty Function; :: thesis:
assume that
A12: dom f1 = dom F and
A13: for x being object st x in dom F holds
for C being Category st C = F . x holds
f1 . x = the carrier' of C and
A14: dom f2 = dom F and
A15: for x being object st x in dom F holds
for C being Category st C = F . x holds
f2 . x = the carrier' of C ; :: thesis:

let x be object ; :: thesis:
assume A16: x in dom F ; :: thesis:
then reconsider C = F . x as Category by Def1;
thus f1 . x = the carrier' of C by A13, A16
.= f2 . x by A15, A16 ; :: thesis:

end;