let S be non empty non void ManySortedSign ; for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2
let U0, U1, U2 be MSAlgebra over S; ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 )
assume that
A1:
U0 is MSSubAlgebra of U1
and
A2:
U1 is MSSubAlgebra of U2
; U0 is MSSubAlgebra of U2
reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def9;
A3:
B0 is opers_closed
by A1, Def9;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A2, Def9;
A4:
B1 is opers_closed
by A2, Def9;
reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def 18;
A5:
the Charact of U1 = Opers (U2,B1)
by A2, Def9;
the Sorts of U0 is MSSubset of U1
by A1, Def9;
then A6:
the Sorts of U0 c= the Sorts of U1
by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U2
by A2, Def9;
then
the Sorts of U1 c= the Sorts of U2
by PBOOLE:def 18;
then
the Sorts of U0 c= the Sorts of U2
by A6, PBOOLE:13;
hence
the Sorts of U0 is MSSubset of U2
by PBOOLE:def 18; MSUALG_2:def 9 for B being MSSubset of U2 st B = the Sorts of U0 holds
( B is opers_closed & the Charact of U0 = Opers (U2,B) )
let B be MSSubset of U2; ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers (U2,B) ) )
set O = the Charact of U0;
set P = Opers (U2,B);
A7:
the Charact of U0 = Opers (U1,B0)
by A1, Def9;
assume A8:
B = the Sorts of U0
; ( B is opers_closed & the Charact of U0 = Opers (U2,B) )
A9:
for o being OperSymbol of S holds B is_closed_on o
proof
let o be
OperSymbol of
S;
B is_closed_on o
A10:
B0 is_closed_on o
by A3;
A11:
B1 is_closed_on o
by A4;
A12:
Den (
o,
U1) =
(Opers (U2,B1)) . o
by A5, MSUALG_1:def 6
.=
o /. B1
by Def8
.=
(Den (o,U2)) | (((B1 #) * the Arity of S) . o)
by A11, Def7
;
A13:
((B0 #) * the Arity of S) . o c= ((B19 #) * the Arity of S) . o
by A6, Th2;
Den (
o,
U0) =
(Opers (U1,B0)) . o
by A7, MSUALG_1:def 6
.=
o /. B0
by Def8
.=
((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o)
by A10, A12, Def7
.=
(Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o))
by RELAT_1:71
.=
(Den (o,U2)) | (((B0 #) * the Arity of S) . o)
by A13, XBOOLE_1:28
;
then
rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= Result (
o,
U0)
by RELAT_1:def 19;
then
rng ((Den (o,U2)) | (((B0 #) * the Arity of S) . o)) c= ( the Sorts of U0 * the ResultSort of S) . o
by MSUALG_1:def 5;
hence
B is_closed_on o
by A8;
verum
end;
hence
B is opers_closed
; the Charact of U0 = Opers (U2,B)
for x being object st x in the carrier' of S holds
the Charact of U0 . x = (Opers (U2,B)) . x
proof
let x be
object ;
( x in the carrier' of S implies the Charact of U0 . x = (Opers (U2,B)) . x )
assume
x in the
carrier' of
S
;
the Charact of U0 . x = (Opers (U2,B)) . x
then reconsider o =
x as
OperSymbol of
S ;
A14:
B0 is_closed_on o
by A3;
A15:
B1 is_closed_on o
by A4;
A16:
Den (
o,
U1) =
(Opers (U2,B1)) . o
by A5, MSUALG_1:def 6
.=
o /. B1
by Def8
.=
(Den (o,U2)) | (((B1 #) * the Arity of S) . o)
by A15, Def7
;
thus the
Charact of
U0 . x =
o /. B0
by A7, Def8
.=
((Den (o,U2)) | (((B1 #) * the Arity of S) . o)) | (((B0 #) * the Arity of S) . o)
by A14, A16, Def7
.=
(Den (o,U2)) | ((((B1 #) * the Arity of S) . o) /\ (((B0 #) * the Arity of S) . o))
by RELAT_1:71
.=
(Den (o,U2)) | (((B #) * the Arity of S) . o)
by A6, A8, Th2, XBOOLE_1:28
.=
o /. B
by A9, Def7
.=
(Opers (U2,B)) . x
by Def8
;
verum
end;
hence
the Charact of U0 = Opers (U2,B)
; verum