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 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. 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 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. 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 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1
let B1 be MSSubset of A1; :: thesis: for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1
let B2 be MSSubset of A2; :: thesis: ( B1 = B2 implies for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1 )
assume A2: B1 = B2 ; :: thesis: for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1
let o be OperSymbol of S; :: thesis: ( B1 is_closed_on o implies o /. B2 = o /. B1 )
assume A3: B1 is_closed_on o ; :: thesis: o /. B2 = o /. B1
hence o /. B2 = (Den (o,A2)) | (((B2 #) * the Arity of S) . o) by A1, A2, Th24, MSUALG_2:def 7
.= (Den (o,A1)) | (((B1 #) * the Arity of S) . o) by A1, A2
.= o /. B1 by A3, MSUALG_2:def 7 ;
:: thesis: verum