let S be non void Signature; :: thesis: for X, Y being V5() ManySortedSet of
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 ; :: 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 SA = the Sorts of A as MSSubset of (FreeMSA X) by MSUALG_2:def 10;
reconsider SB = the Sorts of B as MSSubset of (FreeMSA Y) by MSUALG_2:def 10;
A2:
( SA is opers_closed & SB is opers_closed )
by MSUALG_2:def 10;
now let x be
set ;
:: thesis: ( x in the carrier' of S implies the Charact of A . x = the Charact of B . x )assume
x in the
carrier' of
S
;
:: thesis: the Charact of A . x = the Charact of B . xthen reconsider o =
x as
OperSymbol of
S ;
A3:
(
SA is_closed_on o &
SB is_closed_on o )
by A2, MSUALG_2:def 7;
A4: 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 A3, MSUALG_2:def 8
;
A5: 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 A3, MSUALG_2:def 8
;
A6:
(
SA c= the
Sorts of
(FreeMSA X) &
SB c= the
Sorts of
(FreeMSA Y) & the
Sorts of
(FreeMSA X) is
MSSubset of
(FreeMSA X) & the
Sorts of
(FreeMSA Y) is
MSSubset of
(FreeMSA Y) )
by PBOOLE:def 23;
then A7:
(
((SA # ) * the Arity of S) . o c= ((the Sorts of (FreeMSA X) # ) * the Arity of S) . o &
((SB # ) * the Arity of S) . o c= ((the Sorts of (FreeMSA Y) # ) * the Arity of S) . o )
by MSUALG_2:3;
(
Args o,
(FreeMSA X) = ((the Sorts of (FreeMSA X) # ) * the Arity of S) . o &
Args o,
(FreeMSA Y) = ((the Sorts of (FreeMSA Y) # ) * 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 &
dom (Den o,(FreeMSA Y)) = ((the Sorts of (FreeMSA Y) # ) * the Arity of S) . o )
by FUNCT_2:def 1;
then A8:
(
dom (the Charact of A . o) = ((SA # ) * the Arity of S) . o &
dom (the Charact of B . o) = ((SB # ) * the Arity of S) . o )
by A4, A5, A6, MSUALG_2:3, RELAT_1:91;
now let x be
set ;
:: thesis: ( x in ((SA # ) * the Arity of S) . o implies (the Charact of A . o) . x = (the Charact of B . o) . x )assume A9:
x in ((SA # ) * the Arity of S) . o
;
:: thesis: (the Charact of A . o) . x = (the Charact of B . o) . xthen reconsider p1 =
x as
Element of
Args o,
(FreeMSA X) by A7, MSUALG_1:def 9;
reconsider p2 =
x as
Element of
Args o,
(FreeMSA Y) by A1, A7, A9, MSUALG_1:def 9;
thus (the Charact of A . o) . x =
(Den o,(FreeMSA X)) . p1
by A4, A8, A9, 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, A5, A8, A9, FUNCT_1:70
;
:: thesis: verum end; hence
the
Charact of
A . x = the
Charact of
B . x
by A1, A8, FUNCT_1:9;
:: thesis: 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; :: thesis: verum