let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers (U0,B) = the Charact of U0
let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
Opers (U0,B) = the Charact of U0
let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies Opers (U0,B) = the Charact of U0 )
set f1 = the Charact of U0;
set f2 = Opers (U0,B);
assume A1: B = the Sorts of U0 ; :: thesis: Opers (U0,B) = the Charact of U0
for x being object st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U0,B)) . x
proof
let x be object ; :: thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers (U0,B)) . x )
assume x in the carrier' of S ; :: thesis: the Charact of U0 . x = (Opers (U0,B)) . x
then reconsider o1 = x as OperSymbol of S ;
( the Charact of U0 . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def 6;
hence the Charact of U0 . x = (Opers (U0,B)) . x by A1, Th3; :: thesis: verum
end;
hence Opers (U0,B) = the Charact of U0 ; :: thesis: verum