defpred S1[ object , object ] means \$2 = union { (f . \$1) where f is Element of Bool M : f in A } ;
A1: for x being object st x in I holds
ex y being object st S1[x,y] ;
consider IT being Function such that
A2: dom IT = I and
A3: for x being object st x in I holds
S1[x,IT . x] from reconsider IT = IT as ManySortedSet of I by ;
for i being object st i in I holds
IT . i c= M . i
proof
let i be object ; :: thesis: ( i in I implies IT . i c= M . i )
assume A4: i in I ; :: thesis: IT . i c= M . i
for x being object st x in IT . i holds
x in M . i
proof
let x be object ; :: thesis: ( x in IT . i implies x in M . i )
assume A5: x in IT . i ; :: thesis: x in M . i
IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3, A4;
then consider Y being set such that
A6: x in Y and
A7: Y in { (f . i) where f is Element of Bool M : f in A } by ;
consider ff being Element of Bool M such that
A8: ff . i = Y and
ff in A by A7;
reconsider ff = ff as ManySortedSubset of M ;
ff c= M by PBOOLE:def 18;
then ff . i c= M . i by A4;
hence x in M . i by A6, A8; :: thesis: verum
end;
hence IT . i c= M . i ; :: thesis: verum
end;
then IT c= M ;
then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def 18;
take IT ; :: thesis: for i being set st i in I holds
IT . i = union { (f . i) where f is Element of Bool M : f in A }

thus for i being set st i in I holds
IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3; :: thesis: verum