the Sorts of U2 is MSSubset of U0
by Def9;
then A1:
the Sorts of U2 c= the Sorts of U0
by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0
by Def9;
then
the Sorts of U1 c= the Sorts of U0
by PBOOLE:def 18;
then
the Sorts of U1 (/\) the Sorts of U2 c= the Sorts of U0 (/\) the Sorts of U0
by A1, PBOOLE:21;
then reconsider A = the Sorts of U1 (/\) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;
reconsider E = U0 | A as strict MSSubAlgebra of U0 ;
take
E
; ( the Sorts of E = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) ) ) )
A is opers_closed
proof
reconsider u1 = the
Sorts of
U1,
u2 = the
Sorts of
U2 as
MSSubset of
U0 by Def9;
let o be
OperSymbol of
S;
MSUALG_2:def 6 A is_closed_on o
A2:
dom ((u1 #) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 2;
A3:
dom ((u2 #) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 2;
u2 is
opers_closed
by Def9;
then
u2 is_closed_on o
;
then A4:
rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o
;
dom ((A #) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 2;
then A5:
((A #) * the Arity of S) . o =
(A #) . ( the Arity of S . o)
by FUNCT_1:12
.=
(A #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ((u1 (/\) u2) * (the_arity_of o))
by FINSEQ_2:def 5
.=
(product (u1 * (the_arity_of o))) /\ (product (u2 * (the_arity_of o)))
by Th1
.=
((u1 #) . (the_arity_of o)) /\ (product (u2 * (the_arity_of o)))
by FINSEQ_2:def 5
.=
((u1 #) . (the_arity_of o)) /\ ((u2 #) . (the_arity_of o))
by FINSEQ_2:def 5
.=
((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . (the_arity_of o))
by MSUALG_1:def 1
.=
((u1 #) . ( the Arity of S . o)) /\ ((u2 #) . ( the Arity of S . o))
by MSUALG_1:def 1
.=
(((u1 #) * the Arity of S) . o) /\ ((u2 #) . ( the Arity of S . o))
by A2, FUNCT_1:12
.=
(((u1 #) * the Arity of S) . o) /\ (((u2 #) * the Arity of S) . o)
by A3, FUNCT_1:12
;
then
(Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u2 #) * the Arity of S) . o)) | (((u1 #) * the Arity of S) . o)
by RELAT_1:71;
then
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u2 #) * the Arity of S) . o))
by RELAT_1:70;
then A6:
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o
by A4;
u1 is
opers_closed
by Def9;
then
u1 is_closed_on o
;
then A7:
rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o
;
A8:
dom (u2 * the ResultSort of S) = the
carrier' of
S
by PARTFUN1:def 2;
(Den (o,U0)) | (((A #) * the Arity of S) . o) = ((Den (o,U0)) | (((u1 #) * the Arity of S) . o)) | (((u2 #) * the Arity of S) . o)
by A5, RELAT_1:71;
then
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= rng ((Den (o,U0)) | (((u1 #) * the Arity of S) . o))
by RELAT_1:70;
then
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (u1 * the ResultSort of S) . o
by A7;
then A9:
rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o)
by A6, XBOOLE_1:19;
A10:
dom (A * the ResultSort of S) = the
carrier' of
S
by PARTFUN1:def 2;
dom (u1 * the ResultSort of S) = the
carrier' of
S
by PARTFUN1:def 2;
then ((u1 * the ResultSort of S) . o) /\ ((u2 * the ResultSort of S) . o) =
(u1 . ( the ResultSort of S . o)) /\ ((u2 * the ResultSort of S) . o)
by FUNCT_1:12
.=
(u1 . ( the ResultSort of S . o)) /\ (u2 . ( the ResultSort of S . o))
by A8, FUNCT_1:12
.=
(u1 . (the_result_sort_of o)) /\ (u2 . ( the ResultSort of S . o))
by MSUALG_1:def 2
.=
(u1 . (the_result_sort_of o)) /\ (u2 . (the_result_sort_of o))
by MSUALG_1:def 2
.=
A . (the_result_sort_of o)
by PBOOLE:def 5
.=
A . ( the ResultSort of S . o)
by MSUALG_1:def 2
.=
(A * the ResultSort of S) . o
by A10, FUNCT_1:12
;
hence
A is_closed_on o
by A9;
verum
end;
then
U0 | A = MSAlgebra(# A,(Opers (U0,A)) #)
by Def15;
hence
the Sorts of E = the Sorts of U1 (/\) the Sorts of U2
; for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) )
thus
for B being MSSubset of U0 st B = the Sorts of E holds
( B is opers_closed & the Charact of E = Opers (U0,B) )
by Def9; verum