let S be non empty non void ManySortedSign ; for U0, U1, U2 being MSAlgebra of S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2
let U0, U1, U2 be MSAlgebra of 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, Def10;
A3:
B0 is opers_closed
by A1, Def10;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A2, Def10;
A4:
B1 is opers_closed
by A2, Def10;
reconsider B19 = B1 as MSSubset of U1 by PBOOLE:def 23;
A5:
the Charact of U1 = Opers U2,B1
by A2, Def10;
the Sorts of U0 is MSSubset of U1
by A1, Def10;
then A6:
the Sorts of U0 c= the Sorts of U1
by PBOOLE:def 23;
the Sorts of U1 is MSSubset of U2
by A2, Def10;
then
the Sorts of U1 c= the Sorts of U2
by PBOOLE:def 23;
then
the Sorts of U0 c= the Sorts of U2
by A6, PBOOLE:15;
hence
the Sorts of U0 is MSSubset of U2
by PBOOLE:def 23; MSUALG_2:def 10 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, Def10;
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, Def7;
A11:
B1 is_closed_on o
by A4, Def7;
A12:
Den o,
U1 =
(Opers U2,B1) . o
by A5, MSUALG_1:def 11
.=
o /. B1
by Def9
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A11, Def8
;
A13:
((B0 # ) * the Arity of S) . o c= ((B19 # ) * the Arity of S) . o
by A6, Th3;
Den o,
U0 =
(Opers U1,B0) . o
by A7, MSUALG_1:def 11
.=
o /. B0
by Def9
.=
((Den o,U2) | (((B1 # ) * the Arity of S) . o)) | (((B0 # ) * the Arity of S) . o)
by A10, A12, Def8
.=
(Den o,U2) | ((((B1 # ) * the Arity of S) . o) /\ (((B0 # ) * the Arity of S) . o))
by RELAT_1:100
.=
(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 10;
hence
B is_closed_on o
by A8, Def6;
verum
end;
hence
B is opers_closed
by Def7; the Charact of U0 = Opers U2,B
for x being set st x in the carrier' of S holds
the Charact of U0 . x = (Opers U2,B) . x
proof
let x be
set ;
( 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, Def7;
A15:
B1 is_closed_on o
by A4, Def7;
A16:
Den o,
U1 =
(Opers U2,B1) . o
by A5, MSUALG_1:def 11
.=
o /. B1
by Def9
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A15, Def8
;
thus the
Charact of
U0 . x =
o /. B0
by A7, Def9
.=
((Den o,U2) | (((B1 # ) * the Arity of S) . o)) | (((B0 # ) * the Arity of S) . o)
by A14, A16, Def8
.=
(Den o,U2) | ((((B1 # ) * the Arity of S) . o) /\ (((B0 # ) * the Arity of S) . o))
by RELAT_1:100
.=
(Den o,U2) | (((B # ) * the Arity of S) . o)
by A6, A8, Th3, XBOOLE_1:28
.=
o /. B
by A9, Def8
.=
(Opers U2,B) . x
by Def9
;
verum
end;
hence
the Charact of U0 = Opers U2,B
by PBOOLE:3; verum