reconsider f = id (Bool M) as SetOp of M ;
take f ; :: thesis:
thus f is algebraic :: thesis:

let x be Element of Bool M; :: according to CLOSURE3:def 3 :: thesis:
assume x = f . x ; :: thesis:
set A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ;
{ (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } c= Bool M

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis:
then ex a being Element of Bool M st
( v = f . a & a is V45() & support a is finite & a c= x ) ;
hence v in Bool M ; :: thesis:

end;

then reconsider A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } as SubsetFamily of M ;
take A ; :: thesis:
thus A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis:
let i be Element of I; :: according to PBOOLE:def 21 :: thesis:
thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def 10 :: thesis:

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in x . i ; :: thesis:
then consider a being Element of Bool M such that
A1: y in a . i and
A2: ( a is V45() & support a is finite & a c= x ) by Th7;
a = f . a ;
then a in A by A2;
then a . i in { (g . i) where g is Element of Bool M : g in A } ;
then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def 4;
hence y in (MSUnion A) . i by Def2; :: thesis:

end;

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in (MSUnion A) . i ; :: thesis:
then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2;
then consider Y being set such that
A3: v in Y and
A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def 4;
consider ff being Element of Bool M such that
A5: Y = ff . i and
A6: ff in A by A4;
consider a being Element of Bool M such that
A7: ff = f . a and
a is V45() and
support a is finite and
A8: a c= x by A6;
ff = a by A7;
then ff . i c= x . i by A8;
hence v in x . i by A3, A5; :: thesis:

end;