reconsider S = UAStr(# the carrier of U0, the charact of U0 #) as strict Universal_Algebra by UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;
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 A4, Def6;
hence (Opers (U0,B)) . n = o /. B by Def6
.= the charact of U0 . n by A2, Th4 ;
:: 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 A2, A3, Th4, FINSEQ_1:13; :: thesis: verum

end;

then reconsider S = S as SubAlgebra of U0 by A1, Def7;
take S ; :: thesis: S is strict
thus S is strict ; :: thesis: verum