let U0 be strict Universal_Algebra; :: thesis: GenUnivAlg ([#] the carrier of U0) = U0
set W = GenUnivAlg ([#] the carrier of U0);
A1: the carrier of (GenUnivAlg ([#] the carrier of U0)) is Subset of U0 by Def8;
the carrier of U0 c= the carrier of (GenUnivAlg ([#] the carrier of U0)) by Def13;
then A2: the carrier of U0 = the carrier of (GenUnivAlg ([#] the carrier of U0)) by A1, XBOOLE_0:def 10;
reconsider B = the carrier of (GenUnivAlg ([#] the carrier of U0)) as non empty Subset of U0 by Def8;
A3: ( B is opers_closed & the charact of (GenUnivAlg ([#] the carrier of U0)) = Opers U0,B ) by Def8;
A4: dom the charact of U0 = dom (Opers U0,B) by Def7;
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 A5: 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 5;
(Opers U0,B) . n = o /. B by A4, A5, Def7;
hence the charact of U0 . n = (Opers U0,B) . n by A2, Th7; :: thesis: verum

end;

hence GenUnivAlg ([#] the carrier of U0) = U0 by A2, A3, A4, FINSEQ_1:17; :: thesis: verum