let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: ( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is MSSubAlgebra of U2 )
assume A1:
( U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 )
; :: thesis: U0 is MSSubAlgebra of U2
then
( the Sorts of U0 is MSSubset of U1 & the Sorts of U1 is MSSubset of U2 )
by Def10;
then A2:
( the Sorts of U1 c= the Sorts of U2 & the Sorts of U0 c= the Sorts of U1 )
by PBOOLE:def 23;
then
the Sorts of U0 c= the Sorts of U2
by PBOOLE:15;
hence
the Sorts of U0 is MSSubset of U2
by PBOOLE:def 23; :: according to MSUALG_2:def 10 :: thesis: 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; :: thesis: ( B = the Sorts of U0 implies ( B is opers_closed & the Charact of U0 = Opers U2,B ) )
assume A3:
B = the Sorts of U0
; :: thesis: ( B is opers_closed & the Charact of U0 = Opers U2,B )
reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1, Def10;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1, Def10;
reconsider B1' = B1 as MSSubset of U1 by PBOOLE:def 23;
A4:
( B0 is opers_closed & the Charact of U0 = Opers U1,B0 & B1 is opers_closed & the Charact of U1 = Opers U2,B1 )
by A1, Def10;
A5:
for o being OperSymbol of S holds B is_closed_on o
proof
let o be
OperSymbol of
S;
:: thesis: B is_closed_on o
A6:
(
B0 is_closed_on o &
B1 is_closed_on o )
by A4, Def7;
A7:
Den o,
U1 =
(Opers U2,B1) . o
by A4, MSUALG_1:def 11
.=
o /. B1
by Def9
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A6, Def8
;
A8:
((B0 # ) * the Arity of S) . o c= ((B1' # ) * the Arity of S) . o
by A2, Th3;
Den o,
U0 =
(Opers U1,B0) . o
by A4, MSUALG_1:def 11
.=
o /. B0
by Def9
.=
((Den o,U2) | (((B1 # ) * the Arity of S) . o)) | (((B0 # ) * the Arity of S) . o)
by A6, A7, 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 A8, XBOOLE_1:28
;
then
rng ((Den o,U2) | (((B0 # ) * the Arity of S) . o)) c= Result o,
U0
by RELSET_1:12;
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 A3, Def6;
:: thesis: verum
end;
hence
B is opers_closed
by Def7; :: thesis: the Charact of U0 = Opers U2,B
set O = the Charact of U0;
set P = 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 ;
:: thesis: ( x in the carrier' of S implies the Charact of U0 . x = (Opers U2,B) . x )
assume
x in the
carrier' of
S
;
:: thesis: the Charact of U0 . x = (Opers U2,B) . x
then reconsider o =
x as
OperSymbol of
S ;
A9:
(
B0 is_closed_on o &
B1 is_closed_on o )
by A4, Def7;
A10:
Den o,
U1 =
(Opers U2,B1) . o
by A4, MSUALG_1:def 11
.=
o /. B1
by Def9
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A9, Def8
;
thus the
Charact of
U0 . x =
o /. B0
by A4, Def9
.=
((Den o,U2) | (((B1 # ) * the Arity of S) . o)) | (((B0 # ) * the Arity of S) . o)
by A9, A10, 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 A2, A3, Th3, XBOOLE_1:28
.=
o /. B
by A5, Def8
.=
(Opers U2,B) . x
by Def9
;
:: thesis: verum
end;
hence
the Charact of U0 = Opers U2,B
by PBOOLE:3; :: thesis: verum