let S be non empty non void ManySortedSign ; for A, B being MSAlgebra over S holds
( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
let A, B be MSAlgebra over S; ( A is MSSubAlgebra of B iff A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
thus
( A is MSSubAlgebra of B implies A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) )
( A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) implies A is MSSubAlgebra of B )proof
assume A1:
A is
MSSubAlgebra of
B
;
A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #)
hence
the
Sorts of
A is
MSSubset of
MSAlgebra(# the
Sorts of
B, the
Charact of
B #)
by MSUALG_2:def 9;
MSUALG_2:def 9 for b1 being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of B, the Charact of B #) holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),b1) ) )
thus
for
BB being
MSSubset of
MSAlgebra(# the
Sorts of
B, the
Charact of
B #) st
BB = the
Sorts of
A holds
(
BB is
opers_closed & the
Charact of
A = Opers (
MSAlgebra(# the
Sorts of
B, the
Charact of
B #),
BB) )
verumproof
let BB be
MSSubset of
MSAlgebra(# the
Sorts of
B, the
Charact of
B #);
( BB = the Sorts of A implies ( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) ) )
assume A2:
BB = the
Sorts of
A
;
( BB is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB) )
reconsider bb =
BB as
MSSubset of
B ;
A3:
bb is
opers_closed
by A1, A2, MSUALG_2:def 9;
A4:
BB is
opers_closed
for
o being
object st
o in the
carrier' of
S holds
the
Charact of
A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
proof
let o be
object ;
( o in the carrier' of S implies the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o )
assume
o in the
carrier' of
S
;
the Charact of A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
then reconsider o =
o as
OperSymbol of
S ;
A6:
Den (
o,
B) =
the
Charact of
MSAlgebra(# the
Sorts of
B, the
Charact of
B #)
. o
by MSUALG_1:def 6
.=
Den (
o,
MSAlgebra(# the
Sorts of
B, the
Charact of
B #))
by MSUALG_1:def 6
;
A7:
bb is_closed_on o
by A3;
A8:
BB is_closed_on o
by A4;
(Opers (B,bb)) . o =
o /. bb
by MSUALG_2:def 8
.=
(Den (o,MSAlgebra(# the Sorts of B, the Charact of B #))) | (((BB #) * the Arity of S) . o)
by A6, A7, MSUALG_2:def 7
.=
o /. BB
by A8, MSUALG_2:def 7
.=
(Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
by MSUALG_2:def 8
;
hence
the
Charact of
A . o = (Opers (MSAlgebra(# the Sorts of B, the Charact of B #),BB)) . o
by A1, A2, MSUALG_2:def 9;
verum
end;
hence
(
BB is
opers_closed & the
Charact of
A = Opers (
MSAlgebra(# the
Sorts of
B, the
Charact of
B #),
BB) )
by A4;
verum
end;
end;
assume A9:
A is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #)
; A is MSSubAlgebra of B
hence
the Sorts of A is MSSubset of B
by MSUALG_2:def 9; MSUALG_2:def 9 for b1 being ManySortedSubset of the Sorts of B holds
( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (B,b1) ) )
let C be MSSubset of B; ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (B,C) ) )
assume A10:
C = the Sorts of A
; ( C is opers_closed & the Charact of A = Opers (B,C) )
reconsider CC = C as MSSubset of MSAlgebra(# the Sorts of B, the Charact of B #) ;
A11:
CC is opers_closed
by A9, A10, MSUALG_2:def 9;
A12:
C is opers_closed
for o being object st o in the carrier' of S holds
the Charact of A . o = (Opers (B,C)) . o
proof
let o be
object ;
( o in the carrier' of S implies the Charact of A . o = (Opers (B,C)) . o )
assume
o in the
carrier' of
S
;
the Charact of A . o = (Opers (B,C)) . o
then reconsider o =
o as
OperSymbol of
S ;
A14:
Den (
o,
B) =
the
Charact of
MSAlgebra(# the
Sorts of
B, the
Charact of
B #)
. o
by MSUALG_1:def 6
.=
Den (
o,
MSAlgebra(# the
Sorts of
B, the
Charact of
B #))
by MSUALG_1:def 6
;
A15:
CC is_closed_on o
by A11;
A16:
C is_closed_on o
by A12;
(Opers (MSAlgebra(# the Sorts of B, the Charact of B #),CC)) . o =
o /. CC
by MSUALG_2:def 8
.=
(Den (o,B)) | (((C #) * the Arity of S) . o)
by A14, A15, MSUALG_2:def 7
.=
o /. C
by A16, MSUALG_2:def 7
.=
(Opers (B,C)) . o
by MSUALG_2:def 8
;
hence
the
Charact of
A . o = (Opers (B,C)) . o
by A9, A10, MSUALG_2:def 9;
verum
end;
hence
( C is opers_closed & the Charact of A = Opers (B,C) )
by A12; verum