let U1 be Universal_Algebra; :: thesis: for B being non empty Subset of U1 st B = the carrier of U1 holds
Opers (U1,B) = the charact of U1
let B be non empty Subset of U1; :: thesis: ( B = the carrier of U1 implies Opers (U1,B) = the charact of U1 )
A1: dom (Opers (U1,B)) = dom the charact of U1 by UNIALG_2:def 6;
assume A2: B = the carrier of U1 ; :: thesis: Opers (U1,B) = the charact of U1
now :: thesis: for n being Nat st n in dom the charact of U1 holds
(Opers (U1,B)) . n = the charact of U1 . n
let n be Nat; :: thesis: ( n in dom the charact of U1 implies (Opers (U1,B)) . n = the charact of U1 . n )
assume A3: n in dom the charact of U1 ; :: thesis: (Opers (U1,B)) . n = the charact of U1 . n
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
thus (Opers (U1,B)) . n = o /. B by A1, A3, UNIALG_2:def 6
.= the charact of U1 . n by A2, UNIALG_2:4 ; :: thesis: verum
end;
hence Opers (U1,B) = the charact of U1 by A1; :: thesis: verum