let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0

let U0 be MSAlgebra over S; :: thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0

reconsider A = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSAlgebra over S ;

let U0 be MSAlgebra over S; :: thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0

reconsider A = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSAlgebra over S ;

now :: thesis: ( the Sorts of A is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of A holds

( B is opers_closed & the Charact of A = Opers (U0,B) ) ) )

hence
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0
by Def9; :: thesis: verum( B is opers_closed & the Charact of A = Opers (U0,B) ) ) )

thus
the Sorts of A is MSSubset of U0
by PBOOLE:def 18; :: thesis: for B being MSSubset of U0 st B = the Sorts of A holds

( B is opers_closed & the Charact of A = Opers (U0,B) )

let B be MSSubset of U0; :: thesis: ( B = the Sorts of A implies ( B is opers_closed & the Charact of A = Opers (U0,B) ) )

set f1 = the Charact of A;

set f2 = Opers (U0,B);

assume A1: B = the Sorts of A ; :: thesis: ( B is opers_closed & the Charact of A = Opers (U0,B) )

hence B is opers_closed by Th3; :: thesis: the Charact of A = Opers (U0,B)

for x being object st x in the carrier' of S holds

the Charact of A . x = (Opers (U0,B)) . x

end;( B is opers_closed & the Charact of A = Opers (U0,B) )

let B be MSSubset of U0; :: thesis: ( B = the Sorts of A implies ( B is opers_closed & the Charact of A = Opers (U0,B) ) )

set f1 = the Charact of A;

set f2 = Opers (U0,B);

assume A1: B = the Sorts of A ; :: thesis: ( B is opers_closed & the Charact of A = Opers (U0,B) )

hence B is opers_closed by Th3; :: thesis: the Charact of A = Opers (U0,B)

for x being object st x in the carrier' of S holds

the Charact of A . x = (Opers (U0,B)) . x

proof

hence
the Charact of A = Opers (U0,B)
; :: thesis: verum
let x be object ; :: thesis: ( x in the carrier' of S implies the Charact of A . x = (Opers (U0,B)) . x )

assume x in the carrier' of S ; :: thesis: the Charact of A . x = (Opers (U0,B)) . x

then reconsider o1 = x as Element of the carrier' of S ;

( the Charact of A . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def 6;

hence the Charact of A . x = (Opers (U0,B)) . x by A1, Th3; :: thesis: verum

end;assume x in the carrier' of S ; :: thesis: the Charact of A . x = (Opers (U0,B)) . x

then reconsider o1 = x as Element of the carrier' of S ;

( the Charact of A . o1 = Den (o1,U0) & (Opers (U0,B)) . o1 = o1 /. B ) by Def8, MSUALG_1:def 6;

hence the Charact of A . x = (Opers (U0,B)) . x by A1, Th3; :: thesis: verum