let f be ManySortedSet of J; :: thesis: ( f = Carrier A iff for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & f . j = the carrier of R ) )

hereby :: thesis: ( ( for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & f . j = the carrier of R ) ) implies f = Carrier A )

assume A1: f = Carrier A ; :: thesis: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & f . j = the carrier of R )
then A3: dom f = dom A by Def13;
A4: J = dom f by PARTFUN1:def 2;
let j be set ; :: thesis: ( j in J implies ex R being 1-sorted st
( R = A . j & f . j = the carrier of R ) )
assume j in J ; :: thesis: ex R being 1-sorted st
( R = A . j & f . j = the carrier of R )
hence ex R being 1-sorted st
( R = A . j & f . j = the carrier of R ) by A1, Def13, A4, A3; :: thesis: verum

end;

assume B1: for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & f . j = the carrier of R ) ; :: thesis: f = Carrier A
B0: dom (Carrier A) = dom A by Def13
.= J by PARTFUN1:def 2 ;
B4: J = dom f by PARTFUN1:def 2;
for j being set st j in J holds
f . j = (Carrier A) . j

proof

let j be set ; :: thesis: ( j in J implies f . j = (Carrier A) . j )
assume B3: j in J ; :: thesis: f . j = (Carrier A) . j
then consider R being 1-sorted such that
B2: ( R = A . j & f . j = the carrier of R ) by B1;
J = dom A by PARTFUN1:def 2;
then ex R1 being 1-sorted st
( R1 = A . j & (Carrier A) . j = the carrier of R1 ) by Def13, B3;
hence f . j = (Carrier A) . j by B2; :: thesis: verum

end;

hence f = Carrier A by B0, B4; :: thesis: verum