defpred S₁[ 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 S₁[x,y] ;
consider IT being Function such that
A2: dom IT = I and
A3: for x being object st x in I holds
S₁[x,IT . x] from CLASSES1:sch 1(A1);
reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;
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 A5, TARSKI:def 4;
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