let S be non void Signature; for X, Y being V5() 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 V5() 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 10;
reconsider SA = the Sorts of A as MSSubset of (FreeMSA X) by MSUALG_2:def 10;
A2:
SA is opers_closed
by MSUALG_2:def 10;
A3:
SB is opers_closed
by MSUALG_2:def 10;
now let x be
set ;
( 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 23;
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, MSUALG_2:def 7;
A6: the
Charact of
A . o =
(Opers (FreeMSA X),SA) . o
by MSUALG_2:def 10
.=
o /. SA
by MSUALG_2:def 9
.=
(Den o,(FreeMSA X)) | (((SA # ) * the Arity of S) . o)
by A5, MSUALG_2:def 8
;
Args o,
(FreeMSA X) = ((the Sorts of (FreeMSA X) # ) * the Arity of S) . o
by MSUALG_1:def 9;
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:3, RELAT_1:91;
A8:
(
SB c= the
Sorts of
(FreeMSA Y) & the
Sorts of
(FreeMSA Y) is
MSSubset of
(FreeMSA Y) )
by PBOOLE:def 23;
then A9:
((SB # ) * the Arity of S) . o c= ((the Sorts of (FreeMSA Y) # ) * the Arity of S) . o
by MSUALG_2:3;
A10:
SB is_closed_on o
by A3, MSUALG_2:def 7;
A11: the
Charact of
B . o =
(Opers (FreeMSA Y),SB) . o
by MSUALG_2:def 10
.=
o /. SB
by MSUALG_2:def 9
.=
(Den o,(FreeMSA Y)) | (((SB # ) * the Arity of S) . o)
by A10, MSUALG_2:def 8
;
Args o,
(FreeMSA Y) = ((the Sorts of (FreeMSA Y) # ) * the Arity of S) . o
by MSUALG_1:def 9;
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:3, RELAT_1:91;
A13:
((SA # ) * the Arity of S) . o c= ((the Sorts of (FreeMSA X) # ) * the Arity of S) . o
by A4, MSUALG_2:3;
now let x be
set ;
( 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 9;
reconsider p2 =
x as
Element of
Args o,
(FreeMSA Y) by A1, A9, A14, MSUALG_1:def 9;
thus (the Charact of A . o) . x =
(Den o,(FreeMSA X)) . p1
by A6, A7, A14, FUNCT_1:70
.=
[o,the carrier of S] -tree p1
by INSTALG1:4
.=
(Den o,(FreeMSA Y)) . p2
by INSTALG1:4
.=
(the Charact of B . o) . x
by A1, A11, A12, A14, FUNCT_1:70
;
verum end; hence
the
Charact of
A . x = the
Charact of
B . x
by A1, A7, A12, FUNCT_1:9;
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