let S be non empty non void ManySortedSign ; :: thesis: for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1)
let A1, A2 be MSAlgebra over S; :: thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) implies for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1) )
assume A1: MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) ; :: thesis: for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1)
let B1 be MSSubset of A1; :: thesis: for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1)
let B2 be MSSubset of A2; :: thesis: ( B1 = B2 & B1 is opers_closed implies Opers (A2,B2) = Opers (A1,B1) )
assume A2: ( B1 = B2 & B1 is opers_closed ) ; :: thesis: Opers (A2,B2) = Opers (A1,B1)

now :: thesis: for x being object st x in the carrier' of S holds
(Opers (A2,B2)) . x = (Opers (A1,B1)) . x

let x be object ; :: thesis: ( x in the carrier' of S implies (Opers (A2,B2)) . x = (Opers (A1,B1)) . x )
assume x in the carrier' of S ; :: thesis: (Opers (A2,B2)) . x = (Opers (A1,B1)) . x
then reconsider o = x as OperSymbol of S ;
thus (Opers (A2,B2)) . x = o /. B2 by MSUALG_2:def 8
.= o /. B1 by A1, A2, Th25
.= (Opers (A1,B1)) . x by MSUALG_2:def 8 ; :: thesis: verum

end;

hence Opers (A2,B2) = Opers (A1,B1) ; :: thesis: verum