let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S holds U0 is MSSubAlgebra of U0
let U0 be MSAlgebra of S; :: thesis: U0 is MSSubAlgebra of U0
thus the Sorts of U0 is MSSubset of U0 by PBOOLE:def 23; :: according to MSUALG_2:def 10 :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & the Charact of U0 = Opers U0,B )
let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers U0,B ) )
set f1 = the Charact of U0;
set f2 = Opers U0,B;
assume A1: B = the Sorts of U0 ; :: thesis: ( B is opers_closed & the Charact of U0 = Opers U0,B )
hence B is opers_closed by Th4; :: thesis: the Charact of U0 = Opers U0,B
for x being set st x in the carrier' of S holds
the Charact of U0 . x = (Opers U0,B) . x

proof

let x be set ; :: 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 Def9, MSUALG_1:def 11;
hence the Charact of U0 . x = (Opers U0,B) . x by A1, Th4; :: thesis: verum

end;

hence the Charact of U0 = Opers U0,B by PBOOLE:3; :: thesis: verum