let S be non void Signature; :: thesis: for X, Y being V8() ManySortedSet of the carrier of S
for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

let X, Y be V8() ManySortedSet of the carrier of S; :: thesis: for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

let A be MSSubAlgebra of FreeMSA X; :: thesis: for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

let B be MSSubAlgebra of FreeMSA Y; :: thesis: ( the Sorts of A = the Sorts of B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) )
assume A1: the Sorts of A = the Sorts of B ; :: thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
reconsider SB = the Sorts of B as MSSubset of () by MSUALG_2:def 9;
reconsider SA = the Sorts of A as MSSubset of () by MSUALG_2:def 9;
A2: SA is opers_closed by MSUALG_2:def 9;
A3: SB is opers_closed by MSUALG_2:def 9;
now :: thesis: for x being object st x in the carrier' of S holds
the Charact of A . x = the Charact of B . x
let x be object ; :: thesis: ( x in the carrier' of S implies the Charact of A . x = the Charact of B . x )
A4: ( SA c= the Sorts of () & the Sorts of () is MSSubset of () ) by PBOOLE:def 18;
assume x in the carrier' of S ; :: thesis: the Charact of A . x = the Charact of B . x
then reconsider o = x as OperSymbol of S ;
A5: SA is_closed_on o by A2;
A6: the Charact of A . o = (Opers ((),SA)) . o by MSUALG_2:def 9
.= o /. SA by MSUALG_2:def 8
.= (Den (o,())) | (((SA #) * the Arity of S) . o) by ;
Args (o,()) = (( the Sorts of () #) * the Arity of S) . o by MSUALG_1:def 4;
then dom (Den (o,())) = (( the Sorts of () #) * the Arity of S) . o by FUNCT_2:def 1;
then A7: dom ( the Charact of A . o) = ((SA #) * the Arity of S) . o by ;
A8: ( SB c= the Sorts of () & the Sorts of () is MSSubset of () ) by PBOOLE:def 18;
then A9: ((SB #) * the Arity of S) . o c= (( the Sorts of () #) * the Arity of S) . o by MSUALG_2:2;
A10: SB is_closed_on o by A3;
A11: the Charact of B . o = (Opers ((),SB)) . o by MSUALG_2:def 9
.= o /. SB by MSUALG_2:def 8
.= (Den (o,())) | (((SB #) * the Arity of S) . o) by ;
Args (o,()) = (( the Sorts of () #) * the Arity of S) . o by MSUALG_1:def 4;
then dom (Den (o,())) = (( the Sorts of () #) * the Arity of S) . o by FUNCT_2:def 1;
then A12: dom ( the Charact of B . o) = ((SB #) * the Arity of S) . o by ;
A13: ((SA #) * the Arity of S) . o c= (( the Sorts of () #) * the Arity of S) . o by ;
now :: thesis: for x being object st x in ((SA #) * the Arity of S) . o holds
( the Charact of A . o) . x = ( the Charact of B . o) . x
let x be object ; :: thesis: ( x in ((SA #) * the Arity of S) . o implies ( the Charact of A . o) . x = ( the Charact of B . o) . x )
assume A14: x in ((SA #) * the Arity of S) . o ; :: thesis: ( the Charact of A . o) . x = ( the Charact of B . o) . x
then reconsider p1 = x as Element of Args (o,()) by ;
reconsider p2 = x as Element of Args (o,()) by ;
thus ( the Charact of A . o) . x = (Den (o,())) . p1 by
.= [o, the carrier of S] -tree p1 by INSTALG1:3
.= (Den (o,())) . p2 by INSTALG1:3
.= ( the Charact of B . o) . x by ; :: thesis: verum
end;
hence the Charact of A . x = the Charact of B . x by ; :: thesis: verum
end;
hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by ; :: thesis: verum