let S be non void Signature; for X, Y being non-empty 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 non-empty 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 A be 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 B be MSSubAlgebra of FreeMSA Y; ( 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
; 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 for x being object st x in the carrier' of S holds
the Charact of A . x = the Charact of B . xlet x be
object ;
( 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
;
the Charact of A . x = the Charact of B . xthen 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 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) . xlet x be
object ;
( 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
;
( the Charact of A . o) . x = ( the Charact of B . o) . xthen 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
;
verum end; hence
the
Charact of
A . x = the
Charact of
B . x
by A1, A7, A12, FUNCT_1:2;
verum end;
hence
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
by A1, PBOOLE:3; verum