let X be set ; :: thesis: for S being 1-sorted holds Carrier (X --> S) = X --> the carrier of S
let S be 1-sorted ; :: thesis: Carrier (X --> S) = X --> the carrier of S
A1: dom (Carrier (X --> S)) = dom (X --> S) by Def13
.= dom (X --> the carrier of S) ;

now :: thesis: for x being object st x in dom (Carrier (X --> S)) holds
(Carrier (X --> S)) . x = (X --> the carrier of S) . x

let x be object ; :: thesis: ( x in dom (Carrier (X --> S)) implies (Carrier (X --> S)) . x = (X --> the carrier of S) . x )
assume x in dom (Carrier (X --> S)) ; :: thesis: (Carrier (X --> S)) . x = (X --> the carrier of S) . x
then A2: x in dom (X --> S) by Def13;
then consider R being 1-sorted such that
A4: ( R = (X --> S) . x & (Carrier (X --> S)) . x = the carrier of R ) by Def13;
thus (Carrier (X --> S)) . x = the carrier of S by A2, A4, FUNCOP_1:7
.= (X --> the carrier of S) . x by A2, FUNCOP_1:7 ; :: thesis: verum

end;

hence Carrier (X --> S) = X --> the carrier of S by A1; :: thesis: verum