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 )
assume A1: B = the carrier of U1 ; :: thesis: Opers U1,B = the charact of U1
A2: dom (Opers U1,B) = dom the charact of U1 by UNIALG_2:def 7;

now

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 5;
thus (Opers U1,B) . n = o /. B by A2, A3, UNIALG_2:def 7
.= the charact of U1 . n by A1, UNIALG_2:7 ; :: thesis: verum

end;

hence Opers U1,B = the charact of U1 by A2, FINSEQ_1:17; :: thesis: verum