let X be ManySortedSet of I; :: 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 15;
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 j being object st j in I holds
X . j = (Carrier C) . j
proof
let j be object ; :: thesis: ( j in I implies X . j = (Carrier C) . j )
assume b2: j in I ; :: thesis: X . j = (Carrier C) . j
then reconsider jj = j as Element of I ;
B2: X . j = the carrier of (C . jj) by A2;
I = dom C by PARTFUN1:def 2;
then ex R1 being 1-sorted st
( R1 = C . j & (Carrier C) . j = the carrier of R1 ) by b2, PRALG_1:def 14;
hence X . j = (Carrier C) . j by B2; :: thesis: verum
end;
hence X = Carrier C by PBOOLE:3; :: thesis: verum