set u2 = F .:.: the Sorts of U1;
then
F .:.: the Sorts of U1 c= the Sorts of U2
by PBOOLE:def 2;
then reconsider u2 = F .:.: the Sorts of U1 as non-empty MSSubset of U2 by A2, PBOOLE:def 13, PBOOLE:def 18;
set M = GenMSAlg u2;
reconsider M9 = MSAlgebra(# u2,(Opers (U2,u2)) #) as non-empty MSAlgebra over S by MSUALG_1:def 3;
take
GenMSAlg u2
; the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1
u2 is opers_closed
proof
let o be
OperSymbol of
S;
MSUALG_2:def 6 u2 is_closed_on o
thus
rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o
MSUALG_2:def 5 verumproof
let x be
object ;
TARSKI:def 3 ( not x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) or x in (u2 * the ResultSort of S) . o )
set D =
Den (
o,
U2);
set X =
((u2 #) * the Arity of S) . o;
set ao =
the_arity_of o;
set ro =
the_result_sort_of o;
set ut =
u2 * (the_arity_of o);
set S1 = the
Sorts of
U1;
A8:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
A9:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
then
dom ((u2 #) * the Arity of S) = dom the
Arity of
S
by PARTFUN1:def 2;
then A10:
((u2 #) * the Arity of S) . o =
(u2 #) . ( the Arity of S . o)
by A9, FUNCT_1:12
.=
(u2 #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product (u2 * (the_arity_of o))
by FINSEQ_2:def 5
;
assume
x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o))
;
x in (u2 * the ResultSort of S) . o
then consider a being
object such that A11:
a in dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o))
and A12:
x = ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) . a
by FUNCT_1:def 3;
A13:
x = (Den (o,U2)) . a
by A11, A12, FUNCT_1:47;
dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= dom (Den (o,U2))
by RELAT_1:60;
then reconsider a =
a as
Element of
Args (
o,
U2)
by A11, FUNCT_2:def 1;
defpred S1[
object ,
object ]
means for
s being
SortSymbol of
S st
s = (the_arity_of o) . $1 holds
( $2
in the
Sorts of
U1 . s &
a . $1
= (F . s) . $2 );
A14:
dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= ((u2 #) * the Arity of S) . o
by RELAT_1:58;
then A15:
dom a = dom (u2 * (the_arity_of o))
by A11, A10, CARD_3:9;
A16:
dom u2 = the
carrier of
S
by PARTFUN1:def 2;
A17:
for
y being
object st
y in dom a holds
ex
i being
object st
S1[
y,
i]
proof
let y be
object ;
( y in dom a implies ex i being object st S1[y,i] )
assume A18:
y in dom a
;
ex i being object st S1[y,i]
then A19:
a . y in (u2 * (the_arity_of o)) . y
by A11, A14, A10, A15, CARD_3:9;
dom (u2 * (the_arity_of o)) = dom (the_arity_of o)
by A16, A8, RELAT_1:27;
then
(the_arity_of o) . y in rng (the_arity_of o)
by A15, A18, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . y as
SortSymbol of
S by A8;
A20:
dom (F . s) = the
Sorts of
U1 . s
by FUNCT_2:def 1;
(u2 * (the_arity_of o)) . y =
u2 . ((the_arity_of o) . y)
by A15, A18, FUNCT_1:12
.=
(F . s) .: ( the Sorts of U1 . s)
by PBOOLE:def 20
.=
rng (F . s)
by A20, RELAT_1:113
;
then consider i being
object such that A21:
(
i in the
Sorts of
U1 . s &
a . y = (F . s) . i )
by A20, A19, FUNCT_1:def 3;
take
i
;
S1[y,i]
thus
S1[
y,
i]
by A21;
verum
end;
consider f being
Function such that A22:
(
dom f = dom a & ( for
y being
object st
y in dom a holds
S1[
y,
f . y] ) )
from CLASSES1:sch 1(A17);
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then A23:
dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o)
by A8, RELAT_1:27;
A24:
dom f = dom (the_arity_of o)
by A15, A16, A8, A22, RELAT_1:27;
A25:
for
y being
object st
y in dom ( the Sorts of U1 * (the_arity_of o)) holds
f . y in ( the Sorts of U1 * (the_arity_of o)) . y
Args (
o,
U1)
= product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:3;
then reconsider a1 =
f as
Element of
Args (
o,
U1)
by A24, A23, A25, CARD_3:9;
A27:
dom a1 = dom (the_arity_of o)
by Th6;
(
dom (F # a1) = dom (the_arity_of o) &
dom a = dom (the_arity_of o) )
by Th6;
then
F # a1 = a
by A28, FUNCT_1:2;
then A30:
(F . (the_result_sort_of o)) . ((Den (o,U1)) . a1) = x
by A1, A13;
reconsider g =
F . (the_result_sort_of o) as
Function ;
A31:
dom (F . (the_result_sort_of o)) = the
Sorts of
U1 . (the_result_sort_of o)
by FUNCT_2:def 1;
A32:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
then A33:
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by PARTFUN1:def 2;
Result (
o,
U1) =
( the Sorts of U1 * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . o)
by A32, A33, FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of o)
by MSUALG_1:def 2
;
then
(Den (o,U1)) . a1 in the
Sorts of
U1 . (the_result_sort_of o)
;
then A34:
(Den (o,U1)) . a1 in dom (F . (the_result_sort_of o))
by FUNCT_2:def 1;
dom (u2 * the ResultSort of S) = dom the
ResultSort of
S
by A32, PARTFUN1:def 2;
then (u2 * the ResultSort of S) . o =
u2 . ( the ResultSort of S . o)
by A32, FUNCT_1:12
.=
u2 . (the_result_sort_of o)
by MSUALG_1:def 2
.=
g .: ( the Sorts of U1 . (the_result_sort_of o))
by PBOOLE:def 20
.=
rng g
by A31, RELAT_1:113
;
hence
x in (u2 * the ResultSort of S) . o
by A30, A34, FUNCT_1:def 3;
verum
end;
end;
then
for B being MSSubset of U2 st B = the Sorts of M9 holds
( B is opers_closed & the Charact of M9 = Opers (U2,B) )
;
then A35:
M9 is MSSubAlgebra of U2
by MSUALG_2:def 9;
u2 is MSSubset of M9
by PBOOLE:def 18;
then
GenMSAlg u2 is MSSubAlgebra of M9
by A35, MSUALG_2:def 17;
then
the Sorts of (GenMSAlg u2) is MSSubset of M9
by MSUALG_2:def 9;
then A36:
the Sorts of (GenMSAlg u2) c= u2
by PBOOLE:def 18;
u2 is MSSubset of (GenMSAlg u2)
by MSUALG_2:def 17;
then
u2 c= the Sorts of (GenMSAlg u2)
by PBOOLE:def 18;
hence
the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1
by A36, PBOOLE:146; verum