let f1, f2 be non-empty Function; :: thesis: ( dom f1 = dom F & ( 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 ) & dom f2 = dom F & ( 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 ) implies f1 = f2 )
assume that
A4: dom f1 = dom F and
A5: 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
A6: dom f2 = dom F and
A7: 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: f1 = f2

now :: thesis: for x being object st x in dom F holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in dom F implies f1 . x = f2 . x )
assume A8: x in dom F ; :: thesis: f1 . x = f2 . x
then reconsider C = F . x as Category by Def1;
thus f1 . x = the carrier of C by A5, A8
.= f2 . x by A7, A8 ; :: thesis: verum

end;

hence f1 = f2 by A4, A6; :: thesis: verum