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