let X be ManySortedSet of ; :: thesis: ( X = Carrier C iff for i being Element of I holds X . i = the carrier of (C . i) )
thus ( X = Carrier C implies for i being Element of I holds X . i = the carrier of (C . i) ) :: thesis: ( ( for i being Element of I holds X . i = the carrier of (C . i) ) implies X = Carrier C )

proof

assume A1: X = Carrier C ; :: thesis: for i being Element of I holds X . i = the carrier of (C . i)
let i be Element of I; :: thesis: X . i = the carrier of (C . i)
ex P being 1-sorted st
( P = C . i & X . i = the carrier of P ) by A1, PRALG_1:def 13;
hence X . i = the carrier of (C . i) ; :: thesis: verum

end;

assume A2: for i being Element of I holds X . i = the carrier of (C . i) ; :: thesis: X = Carrier C
for i being set st i in I holds
ex P being 1-sorted st
( P = C . i & X . i = the carrier of P )

proof

let i be set ; :: thesis: ( i in I implies ex P being 1-sorted st
( P = C . i & X . i = the carrier of P ) )
assume i in I ; :: thesis: ex P being 1-sorted st
( P = C . i & X . i = the carrier of P )
then reconsider i = i as Element of I ;
take C . i ; :: thesis: ( C . i = C . i & X . i = the carrier of (C . i) )
thus ( C . i = C . i & X . i = the carrier of (C . i) ) by A2; :: thesis: verum

end;

hence X = Carrier C by PRALG_1:def 13; :: thesis: verum