let U0 be strict Universal_Algebra; :: thesis: GenUnivAlg ([#] the carrier of U0) = U0

set W = GenUnivAlg ([#] the carrier of U0);

reconsider B = the carrier of (GenUnivAlg ([#] the carrier of U0)) as non empty Subset of U0 by Def7;

( the carrier of (GenUnivAlg ([#] the carrier of U0)) is Subset of U0 & the carrier of U0 c= the carrier of (GenUnivAlg ([#] the carrier of U0)) ) by Def7, Def12;

then A1: the carrier of U0 = the carrier of (GenUnivAlg ([#] the carrier of U0)) ;

A2: dom the charact of U0 = dom (Opers (U0,B)) by Def6;

A3: for n being Nat st n in dom the charact of U0 holds

the charact of U0 . n = (Opers (U0,B)) . n

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

set W = GenUnivAlg ([#] the carrier of U0);

reconsider B = the carrier of (GenUnivAlg ([#] the carrier of U0)) as non empty Subset of U0 by Def7;

( the carrier of (GenUnivAlg ([#] the carrier of U0)) is Subset of U0 & the carrier of U0 c= the carrier of (GenUnivAlg ([#] the carrier of U0)) ) by Def7, Def12;

then A1: the carrier of U0 = the carrier of (GenUnivAlg ([#] the carrier of U0)) ;

A2: dom the charact of U0 = dom (Opers (U0,B)) by Def6;

A3: for n being Nat st n in dom the charact of U0 holds

the charact of U0 . n = (Opers (U0,B)) . n

proof

the charact of (GenUnivAlg ([#] the carrier of U0)) = Opers (U0,B)
by Def7;
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 A2, A4, Def6;

hence the charact of U0 . n = (Opers (U0,B)) . n by A1, Th4; :: thesis: verum

end;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 A2, A4, Def6;

hence the charact of U0 . n = (Opers (U0,B)) . n by A1, Th4; :: thesis: verum

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