let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let A be OSSubset of OU0; :: thesis: OSConstants OU0 = OSCl (Constants OU0)

A1: now :: thesis: for i being set st i in the carrier of S1 holds
(OSConstants OU0) . i = (OSCl (Constants OU0)) . i

let i be set ; :: thesis: ( i in the carrier of S1 implies (OSConstants OU0) . i = (OSCl (Constants OU0)) . i )
assume i in the carrier of S1 ; :: thesis: (OSConstants OU0) . i = (OSCl (Constants OU0)) . i
then reconsider s = i as SortSymbol of S1 ;
set c1 = { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
set c2 = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ;
for x being object holds
( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } )

proof

let x be object ; :: thesis: ( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } )

hereby :: thesis: ( x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } )

assume x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A2: x = (Constants OU0) . s1 and
A3: s1 <= s ;
x = Constants (OU0,s1) by A2, MSUALG_2:def 4;
hence x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by A3; :: thesis: verum

end;

assume x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; :: thesis: x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s }
then consider s1 being SortSymbol of S1 such that
A4: x = Constants (OU0,s1) and
A5: s1 <= s ;
x = (Constants OU0) . s1 by A4, MSUALG_2:def 4;
hence x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } by A5; :: thesis: verum

end;

then A6: { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by TARSKI:2;
(OSConstants OU0) . s = OSConstants (OU0,s) by Def5
.= (OSCl (Constants OU0)) . s by A6, Def4 ;
hence (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ; :: thesis: verum

end;

then for i being object st i in the carrier of S1 holds
(OSCl (Constants OU0)) . i c= (OSConstants OU0) . i ;
then A7: OSCl (Constants OU0) c= OSConstants OU0 ;
for i being object st i in the carrier of S1 holds
(OSConstants OU0) . i c= (OSCl (Constants OU0)) . i by A1;
then OSConstants OU0 c= OSCl (Constants OU0) ;
hence OSConstants OU0 = OSCl (Constants OU0) by A7, PBOOLE:146; :: thesis: verum