let S be non empty non void ManySortedSign ; :: thesis: for MA being strict non-empty MSAlgebra over S

for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let MA be strict non-empty MSAlgebra over S; :: thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let F be SubsetFamily of the Sorts of MA; :: thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed )

assume A1: F c= SubSort MA ; :: thesis: for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let B be MSSubset of MA; :: thesis: ( B = meet |:F:| implies B is opers_closed )

assume A2: B = meet |:F:| ; :: thesis: B is opers_closed

for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let MA be strict non-empty MSAlgebra over S; :: thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let F be SubsetFamily of the Sorts of MA; :: thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed )

assume A1: F c= SubSort MA ; :: thesis: for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

let B be MSSubset of MA; :: thesis: ( B = meet |:F:| implies B is opers_closed )

assume A2: B = meet |:F:| ; :: thesis: B is opers_closed

per cases
( F = {} or F <> {} )
;

end;

suppose A3:
F = {}
; :: thesis: B is opers_closed

set Q = the Sorts of MA;

reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA ;

set I = the carrier of S;

FF = EmptyMS the carrier of S by A3;

then A4: the Sorts of MA = B by A2, MSSUBFAM:41;

reconsider Q = the Sorts of MA as MSSubset of MA by PBOOLE:def 18;

for o being OperSymbol of S holds Q is_closed_on o

end;reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA ;

set I = the carrier of S;

FF = EmptyMS the carrier of S by A3;

then A4: the Sorts of MA = B by A2, MSSUBFAM:41;

reconsider Q = the Sorts of MA as MSSubset of MA by PBOOLE:def 18;

for o being OperSymbol of S holds Q is_closed_on o

proof

hence
B is opers_closed
by A4; :: thesis: verum
let o be OperSymbol of S; :: thesis: Q is_closed_on o

A5: ( the ResultSort of S . o = the_result_sort_of o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 2;

Result (o,MA) = (Q * the ResultSort of S) . o by MSUALG_1:def 5

.= Q . (the_result_sort_of o) by A5, FUNCT_1:13 ;

then A6: rng ((Den (o,MA)) | ((Q #) . (the_arity_of o))) c= Q . (the_result_sort_of o) by RELAT_1:def 19;

( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 1;

then A7: ((Q #) * the Arity of S) . o = (Q #) . (the_arity_of o) by FUNCT_1:13;

(Q * the ResultSort of S) . o = Q . (the_result_sort_of o) by A5, FUNCT_1:13;

hence Q is_closed_on o by A7, A6; :: thesis: verum

end;A5: ( the ResultSort of S . o = the_result_sort_of o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 2;

Result (o,MA) = (Q * the ResultSort of S) . o by MSUALG_1:def 5

.= Q . (the_result_sort_of o) by A5, FUNCT_1:13 ;

then A6: rng ((Den (o,MA)) | ((Q #) . (the_arity_of o))) c= Q . (the_result_sort_of o) by RELAT_1:def 19;

( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 1;

then A7: ((Q #) * the Arity of S) . o = (Q #) . (the_arity_of o) by FUNCT_1:13;

(Q * the ResultSort of S) . o = Q . (the_result_sort_of o) by A5, FUNCT_1:13;

hence Q is_closed_on o by A7, A6; :: thesis: verum

suppose A8:
F <> {}
; :: thesis: B is opers_closed

set SS = S;

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: B is_closed_on o

set i = the_result_sort_of o;

A9: the ResultSort of S . o = the_result_sort_of o by MSUALG_1:def 2;

A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 1;

then A11: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_1:13;

Result (o,MA) = ( the Sorts of MA * the ResultSort of S) . o by MSUALG_1:def 5

.= the Sorts of MA . (the_result_sort_of o) by A9, A10, FUNCT_1:13 ;

then A12: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the Sorts of MA . (the_result_sort_of o) by RELAT_1:def 19;

A13: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o)

hence B is_closed_on o by A11, A13; :: thesis: verum

end;let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis: B is_closed_on o

set i = the_result_sort_of o;

A9: the ResultSort of S . o = the_result_sort_of o by MSUALG_1:def 2;

A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def 1, MSUALG_1:def 1;

then A11: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_1:13;

Result (o,MA) = ( the Sorts of MA * the ResultSort of S) . o by MSUALG_1:def 5

.= the Sorts of MA . (the_result_sort_of o) by A9, A10, FUNCT_1:13 ;

then A12: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the Sorts of MA . (the_result_sort_of o) by RELAT_1:def 19;

A13: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o)

proof

(B * the ResultSort of S) . o = B . (the_result_sort_of o)
by A9, A10, FUNCT_1:13;
consider Q being Subset-Family of ( the Sorts of MA . (the_result_sort_of o)) such that

A14: Q = |:F:| . (the_result_sort_of o) and

A15: B . (the_result_sort_of o) = Intersect Q by A2, MSSUBFAM:def 1;

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) )

assume A16: v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) ; :: thesis: v in B . (the_result_sort_of o)

then consider p being object such that

A17: p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o))) and

A18: v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p by FUNCT_1:def 3;

for Y being set st Y in Q holds

v in Y

end;A14: Q = |:F:| . (the_result_sort_of o) and

A15: B . (the_result_sort_of o) = Intersect Q by A2, MSSUBFAM:def 1;

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) )

assume A16: v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) ; :: thesis: v in B . (the_result_sort_of o)

then consider p being object such that

A17: p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o))) and

A18: v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p by FUNCT_1:def 3;

for Y being set st Y in Q holds

v in Y

proof

hence
v in B . (the_result_sort_of o)
by A12, A16, A15, SETFAM_1:43; :: thesis: verum
A19:
|:F:| . (the_result_sort_of o) = { (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F }
by A8, CLOSURE2:14;

let Y be set ; :: thesis: ( Y in Q implies v in Y )

assume Y in Q ; :: thesis: v in Y

then consider xx being Element of Bool the Sorts of MA such that

A20: Y = xx . (the_result_sort_of o) and

A21: xx in F by A14, A19;

reconsider xx = xx as MSSubset of MA ;

xx is opers_closed by A1, A21, MSUALG_2:14;

then xx is_closed_on o ;

then A22: rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o ;

B c= xx by A2, A21, CLOSURE2:21, MSSUBFAM:43;

then (Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o) by MSUALG_2:2, RELAT_1:75;

then A23: dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by RELAT_1:11;

A24: v = (Den (o,MA)) . p by A17, A18, FUNCT_1:47;

then v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p by A11, A17, A23, FUNCT_1:47;

then v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by A11, A17, A23, FUNCT_1:def 3;

then (Den (o,MA)) . p in (xx * the ResultSort of S) . o by A22, A24;

then (Den (o,MA)) . p in xx . ( the ResultSort of S . o) by A10, FUNCT_1:13;

then (Den (o,MA)) . p in xx . (the_result_sort_of o) by MSUALG_1:def 2;

hence v in Y by A17, A18, A20, FUNCT_1:47; :: thesis: verum

end;let Y be set ; :: thesis: ( Y in Q implies v in Y )

assume Y in Q ; :: thesis: v in Y

then consider xx being Element of Bool the Sorts of MA such that

A20: Y = xx . (the_result_sort_of o) and

A21: xx in F by A14, A19;

reconsider xx = xx as MSSubset of MA ;

xx is opers_closed by A1, A21, MSUALG_2:14;

then xx is_closed_on o ;

then A22: rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o ;

B c= xx by A2, A21, CLOSURE2:21, MSSUBFAM:43;

then (Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o) by MSUALG_2:2, RELAT_1:75;

then A23: dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by RELAT_1:11;

A24: v = (Den (o,MA)) . p by A17, A18, FUNCT_1:47;

then v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p by A11, A17, A23, FUNCT_1:47;

then v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by A11, A17, A23, FUNCT_1:def 3;

then (Den (o,MA)) . p in (xx * the ResultSort of S) . o by A22, A24;

then (Den (o,MA)) . p in xx . ( the ResultSort of S . o) by A10, FUNCT_1:13;

then (Den (o,MA)) . p in xx . (the_result_sort_of o) by MSUALG_1:def 2;

hence v in Y by A17, A18, A20, FUNCT_1:47; :: thesis: verum

hence B is_closed_on o by A11, A13; :: thesis: verum