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 (FreeMSA Y) by MSUALG_2:def 9;

reconsider SA = the Sorts of A as MSSubset of (FreeMSA X) 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;

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 (FreeMSA Y) by MSUALG_2:def 9;

reconsider SA = the Sorts of A as MSSubset of (FreeMSA X) 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

hence
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
by A1, PBOOLE:3; :: thesis: verumthe 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 (FreeMSA X) & the Sorts of (FreeMSA X) is MSSubset of (FreeMSA X) ) 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 ((FreeMSA X),SA)) . o by MSUALG_2:def 9

.= o /. SA by MSUALG_2:def 8

.= (Den (o,(FreeMSA X))) | (((SA #) * the Arity of S) . o) by A5, MSUALG_2:def 7 ;

Args (o,(FreeMSA X)) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by MSUALG_1:def 4;

then dom (Den (o,(FreeMSA X))) = (( the Sorts of (FreeMSA X) #) * 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 A6, A4, MSUALG_2:2, RELAT_1:62;

A8: ( SB c= the Sorts of (FreeMSA Y) & the Sorts of (FreeMSA Y) is MSSubset of (FreeMSA Y) ) by PBOOLE:def 18;

then A9: ((SB #) * the Arity of S) . o c= (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_2:2;

A10: SB is_closed_on o by A3;

A11: the Charact of B . o = (Opers ((FreeMSA Y),SB)) . o by MSUALG_2:def 9

.= o /. SB by MSUALG_2:def 8

.= (Den (o,(FreeMSA Y))) | (((SB #) * the Arity of S) . o) by A10, MSUALG_2:def 7 ;

Args (o,(FreeMSA Y)) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_1:def 4;

then dom (Den (o,(FreeMSA Y))) = (( the Sorts of (FreeMSA Y) #) * 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 A11, A8, MSUALG_2:2, RELAT_1:62;

A13: ((SA #) * the Arity of S) . o c= (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by A4, MSUALG_2:2;

end;A4: ( SA c= the Sorts of (FreeMSA X) & the Sorts of (FreeMSA X) is MSSubset of (FreeMSA X) ) 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 ((FreeMSA X),SA)) . o by MSUALG_2:def 9

.= o /. SA by MSUALG_2:def 8

.= (Den (o,(FreeMSA X))) | (((SA #) * the Arity of S) . o) by A5, MSUALG_2:def 7 ;

Args (o,(FreeMSA X)) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by MSUALG_1:def 4;

then dom (Den (o,(FreeMSA X))) = (( the Sorts of (FreeMSA X) #) * 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 A6, A4, MSUALG_2:2, RELAT_1:62;

A8: ( SB c= the Sorts of (FreeMSA Y) & the Sorts of (FreeMSA Y) is MSSubset of (FreeMSA Y) ) by PBOOLE:def 18;

then A9: ((SB #) * the Arity of S) . o c= (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_2:2;

A10: SB is_closed_on o by A3;

A11: the Charact of B . o = (Opers ((FreeMSA Y),SB)) . o by MSUALG_2:def 9

.= o /. SB by MSUALG_2:def 8

.= (Den (o,(FreeMSA Y))) | (((SB #) * the Arity of S) . o) by A10, MSUALG_2:def 7 ;

Args (o,(FreeMSA Y)) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_1:def 4;

then dom (Den (o,(FreeMSA Y))) = (( the Sorts of (FreeMSA Y) #) * 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 A11, A8, MSUALG_2:2, RELAT_1:62;

A13: ((SA #) * the Arity of S) . o c= (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by A4, MSUALG_2:2;

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

hence
the Charact of A . x = the Charact of B . x
by A1, A7, A12, FUNCT_1:2; :: thesis: verum( 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,(FreeMSA X)) by A13, MSUALG_1:def 4;

reconsider p2 = x as Element of Args (o,(FreeMSA Y)) by A1, A9, A14, MSUALG_1:def 4;

thus ( the Charact of A . o) . x = (Den (o,(FreeMSA X))) . p1 by A6, A7, A14, FUNCT_1:47

.= [o, the carrier of S] -tree p1 by INSTALG1:3

.= (Den (o,(FreeMSA Y))) . p2 by INSTALG1:3

.= ( the Charact of B . o) . x by A1, A11, A12, A14, FUNCT_1:47 ; :: thesis: verum

end;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,(FreeMSA X)) by A13, MSUALG_1:def 4;

reconsider p2 = x as Element of Args (o,(FreeMSA Y)) by A1, A9, A14, MSUALG_1:def 4;

thus ( the Charact of A . o) . x = (Den (o,(FreeMSA X))) . p1 by A6, A7, A14, FUNCT_1:47

.= [o, the carrier of S] -tree p1 by INSTALG1:3

.= (Den (o,(FreeMSA Y))) . p2 by INSTALG1:3

.= ( the Charact of B . o) . x by A1, A11, A12, A14, FUNCT_1:47 ; :: thesis: verum