let S be non empty non void ManySortedSign ; for U0 being MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2
let U0 be MSAlgebra of S; for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds
U1 is MSSubAlgebra of U2
let U1, U2 be MSSubAlgebra of U0; ( the Sorts of U1 c= the Sorts of U2 implies U1 is MSSubAlgebra of U2 )
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by Def10;
assume A1:
the Sorts of U1 c= the Sorts of U2
; U1 is MSSubAlgebra of U2
hence
the Sorts of U1 is MSSubset of U2
by PBOOLE:def 23; MSUALG_2:def 10 for B being MSSubset of U2 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U2,B )
let B be MSSubset of U2; ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers U2,B ) )
A2:
B1 is opers_closed
by Def10;
set O = the Charact of U1;
set P = Opers U2,B;
A3:
the Charact of U1 = Opers U0,B1
by Def10;
A4:
B2 is opers_closed
by Def10;
A5:
the Charact of U2 = Opers U0,B2
by Def10;
assume A6:
B = the Sorts of U1
; ( B is opers_closed & the Charact of U1 = Opers U2,B )
A7:
for o being OperSymbol of S holds B is_closed_on o
proof
let o be
OperSymbol of
S;
B is_closed_on o
A8:
B1 is_closed_on o
by A2, Def7;
A9:
B2 is_closed_on o
by A4, Def7;
A10:
Den o,
U2 =
(Opers U0,B2) . o
by A5, MSUALG_1:def 11
.=
o /. B2
by Def9
.=
(Den o,U0) | (((B2 # ) * the Arity of S) . o)
by A9, Def8
;
Den o,
U1 =
(Opers U0,B1) . o
by A3, MSUALG_1:def 11
.=
o /. B1
by Def9
.=
(Den o,U0) | (((B1 # ) * the Arity of S) . o)
by A8, Def8
.=
(Den o,U0) | ((((B2 # ) * the Arity of S) . o) /\ (((B1 # ) * the Arity of S) . o))
by A1, Th3, XBOOLE_1:28
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A10, RELAT_1:100
;
then
rng ((Den o,U2) | (((B1 # ) * the Arity of S) . o)) c= Result o,
U1
by RELAT_1:def 19;
then
rng ((Den o,U2) | (((B1 # ) * the Arity of S) . o)) c= (the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 10;
hence
B is_closed_on o
by A6, Def6;
verum
end;
hence
B is opers_closed
by Def7; the Charact of U1 = Opers U2,B
for x being set st x in the carrier' of S holds
the Charact of U1 . x = (Opers U2,B) . x
proof
let x be
set ;
( x in the carrier' of S implies the Charact of U1 . x = (Opers U2,B) . x )
assume
x in the
carrier' of
S
;
the Charact of U1 . x = (Opers U2,B) . x
then reconsider o =
x as
OperSymbol of
S ;
A11:
B1 is_closed_on o
by A2, Def7;
A12:
B2 is_closed_on o
by A4, Def7;
A13:
Den o,
U2 =
(Opers U0,B2) . o
by A5, MSUALG_1:def 11
.=
o /. B2
by Def9
.=
(Den o,U0) | (((B2 # ) * the Arity of S) . o)
by A12, Def8
;
thus the
Charact of
U1 . x =
o /. B1
by A3, Def9
.=
(Den o,U0) | (((B1 # ) * the Arity of S) . o)
by A11, Def8
.=
(Den o,U0) | ((((B2 # ) * the Arity of S) . o) /\ (((B1 # ) * the Arity of S) . o))
by A1, Th3, XBOOLE_1:28
.=
(Den o,U2) | (((B1 # ) * the Arity of S) . o)
by A13, RELAT_1:100
.=
o /. B
by A6, A7, Def8
.=
(Opers U2,B) . x
by Def9
;
verum
end;
hence
the Charact of U1 = Opers U2,B
by PBOOLE:3; verum