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

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

hence
Carrier (M --> S) = M --> the carrier of S
by PBOOLE:3; :: thesis: verum(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;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