let X be set ; :: thesis: for C being Category holds
( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )
let C be Category; :: thesis: ( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )
A2: dom (Objs (X --> C)) = dom (X --> C) by Def2;

now :: thesis: for a being object st a in dom (Objs (X --> C)) holds
(Objs (X --> C)) . a = the carrier of C

let a be object ; :: thesis: ( a in dom (Objs (X --> C)) implies (Objs (X --> C)) . a = the carrier of C )
assume A3: a in dom (Objs (X --> C)) ; :: thesis: (Objs (X --> C)) . a = the carrier of C
then (X --> C) . a = C by A2, FUNCOP_1:7;
hence (Objs (X --> C)) . a = the carrier of C by A2, A3, Def2; :: thesis: verum

end;

hence Objs (X --> C) = X --> the carrier of C by A2, FUNCOP_1:11; :: thesis: Mphs (X --> C) = X --> the carrier' of C
A4: dom (Mphs (X --> C)) = dom (X --> C) by Def3;

now :: thesis: for a being object st a in dom (Mphs (X --> C)) holds
(Mphs (X --> C)) . a = the carrier' of C

let a be object ; :: thesis: ( a in dom (Mphs (X --> C)) implies (Mphs (X --> C)) . a = the carrier' of C )
assume A5: a in dom (Mphs (X --> C)) ; :: thesis: (Mphs (X --> C)) . a = the carrier' of C
then (X --> C) . a = C by A4, FUNCOP_1:7;
hence (Mphs (X --> C)) . a = the carrier' of C by A4, A5, Def3; :: thesis: verum

end;

hence Mphs (X --> C) = X --> the carrier' of C by A4, FUNCOP_1:11; :: thesis: verum