let S be 1-sorted ; :: thesis: for M being set holds Carrier (M --> S) = M --> the carrier of S
let M be set ; :: thesis: Carrier (M --> S) = M --> the carrier of S

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

let i be object ; :: thesis: ( i in M implies (Carrier (M --> S)) . i = (M --> the carrier of S) . i )
assume A1: i in M ; :: thesis: (Carrier (M --> S)) . i = (M --> the carrier of S) . i
then ( (M --> S) . i = S & ex R being 1-sorted st
( R = (M --> S) . i & (Carrier (M --> S)) . i = the carrier of R ) ) by FUNCOP_1:7, PRALG_1:def 15;
hence (Carrier (M --> S)) . i = (M --> the carrier of S) . i by A1, FUNCOP_1:7; :: thesis: verum

end;

hence Carrier (M --> S) = M --> the carrier of S by PBOOLE:3; :: thesis: verum