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 ) )

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

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 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 ) ) 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;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

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

hence
f = Carrier A
by B0, B4; :: thesis: verum
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;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