reconsider S = UAStr(# the carrier of U0, the charact of U0 #) as strict Universal_Algebra by ;
A1: the carrier of S c= the carrier of U0 ;
for B being non empty Subset of U0 st B = the carrier of S holds
( the charact of S = Opers (U0,B) & B is opers_closed )
proof
let B be non empty Subset of U0; :: thesis: ( B = the carrier of S implies ( the charact of S = Opers (U0,B) & B is opers_closed ) )
assume A2: B = the carrier of S ; :: thesis: ( the charact of S = Opers (U0,B) & B is opers_closed )
A3: now :: thesis: for n being Nat st n in dom the charact of U0 holds
(Opers (U0,B)) . n = the charact of U0 . n
let n be Nat; :: thesis: ( n in dom the charact of U0 implies (Opers (U0,B)) . n = the charact of U0 . n )
assume A4: n in dom the charact of U0 ; :: thesis: (Opers (U0,B)) . n = the charact of U0 . n
then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
n in dom (Opers (U0,B)) by ;
hence (Opers (U0,B)) . n = o /. B by Def6
.= the charact of U0 . n by ;
:: thesis: verum
end;
dom the charact of U0 = dom (Opers (U0,B)) by Def6;
hence ( the charact of S = Opers (U0,B) & B is opers_closed ) by ; :: thesis: verum
end;
then reconsider S = S as SubAlgebra of U0 by ;
take S ; :: thesis: S is strict
thus S is strict ; :: thesis: verum