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 )

take S ; :: thesis: S is strict

thus S is strict ; :: thesis: verum

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

then reconsider S = S as SubAlgebra of U0 by A1, Def7;
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 )

hence ( the charact of S = Opers (U0,B) & B is opers_closed ) by A2, A3, Th4, FINSEQ_1:13; :: thesis: verum

end;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

dom the charact of U0 = dom (Opers (U0,B))
by Def6;(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;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

hence ( the charact of S = Opers (U0,B) & B is opers_closed ) by A2, A3, Th4, FINSEQ_1:13; :: thesis: verum

take S ; :: thesis: S is strict

thus S is strict ; :: thesis: verum