reconsider L = product OAF as non-empty MSAlgebra of S ;
deffunc H1( SortSymbol of S) -> set = { f where f is Element of product (Carrier (OAF,$1)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . $1) . (f . i) = f . j } ;
consider C being ManySortedSet of the carrier of S such that
A1:
for s being SortSymbol of S holds C . s = H1(s)
from PBOOLE:sch 5();
for i being set st i in the carrier of S holds
C . i c= (SORTS OAF) . i
then
C c= SORTS OAF
by PBOOLE:def 2;
then reconsider C = C as ManySortedSubset of SORTS OAF by PBOOLE:def 18;
reconsider C = C as MSSubset of (product OAF) by PRALG_2:12;
for o being OperSymbol of S holds C is_closed_on o
proof
let o be
OperSymbol of
S;
C is_closed_on o
rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o
proof
reconsider MS =
C as
ManySortedSet of the
carrier of
S ;
reconsider K =
(Den (o,(product OAF))) | (((C #) * the Arity of S) . o) as
Function ;
let x be
set ;
TARSKI:def 3 ( not x in rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) or x in (C * the ResultSort of S) . o )
A3:
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
assume A4:
x in rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o))
;
x in (C * the ResultSort of S) . o
then consider y being
set such that A5:
y in dom K
and A6:
x = K . y
by FUNCT_1:def 3;
A7:
dom K = (dom (Den (o,(product OAF)))) /\ (((C #) * the Arity of S) . o)
by RELAT_1:61;
then
y in ((C #) * the Arity of S) . o
by A5, XBOOLE_0:def 4;
then
y in (C #) . ( the Arity of S . o)
by A3, FUNCT_1:13;
then
y in (C #) . (the_arity_of o)
by MSUALG_1:def 1;
then A8:
y in product (MS * (the_arity_of o))
by FINSEQ_2:def 5;
x in Result (
o,
(product OAF))
by A4;
then
(
dom the
ResultSort of
S = the
carrier' of
S &
x in ( the Sorts of (product OAF) * the ResultSort of S) . o )
by FUNCT_2:def 1, MSUALG_1:def 5;
then
x in the
Sorts of
(product OAF) . ( the ResultSort of S . o)
by FUNCT_1:13;
then A9:
x in (SORTS OAF) . ( the ResultSort of S . o)
by PRALG_2:12;
then reconsider x1 =
x as
Function ;
x in (SORTS OAF) . (the_result_sort_of o)
by A9, MSUALG_1:def 2;
then A10:
x is
Element of
product (Carrier (OAF,(the_result_sort_of o)))
by PRALG_2:def 10;
A11:
y in dom (Den (o,(product OAF)))
by A5, A7, XBOOLE_0:def 4;
now let s be
SortSymbol of
S;
x in C . (the_result_sort_of o)
for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
proof
reconsider OPE =
(OPS OAF) . o as
Function ;
A12:
Den (
o,
(product OAF)) =
the
Charact of
(product OAF) . o
by MSUALG_1:def 6
.=
(OPS OAF) . o
by PRALG_2:12
;
reconsider y =
y as
Function by A8;
let i,
j be
Element of
P;
( i >= j implies ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j )
assume A13:
i >= j
;
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
reconsider Co =
commute y as
Function ;
set y1 =
(commute y) . i;
A14:
dom y = dom (MS * (the_arity_of o))
by A8, CARD_3:9;
A15:
rng (the_arity_of o) c= dom MS
then A16:
dom y = dom (the_arity_of o)
by A14, RELAT_1:27;
then A17:
dom y = Seg (len (the_arity_of o))
by FINSEQ_1:def 3;
rng y c= Funcs ( the
carrier of
P,
|.OAF.|)
proof
let z be
set ;
TARSKI:def 3 ( not z in rng y or z in Funcs ( the carrier of P,|.OAF.|) )
assume
z in rng y
;
z in Funcs ( the carrier of P,|.OAF.|)
then consider n being
set such that A18:
n in dom y
and A19:
z = y . n
by FUNCT_1:def 3;
A20:
n in dom (MS * (the_arity_of o))
by A8, A18, CARD_3:9;
then
n in dom (the_arity_of o)
by A15, RELAT_1:27;
then
(the_arity_of o) . n = (the_arity_of o) /. n
by PARTFUN1:def 6;
then reconsider Pa =
(the_arity_of o) . n as
SortSymbol of
S ;
z in (MS * (the_arity_of o)) . n
by A8, A19, A20, CARD_3:9;
then
z in MS . ((the_arity_of o) . n)
by A20, FUNCT_1:12;
then
z in { f where f is Element of product (Carrier (OAF,Pa)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pa) . (f . i) = f . j }
by A1;
then A21:
ex
z9 being
Element of
product (Carrier (OAF,Pa)) st
(
z9 = z & ( for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . Pa) . (z9 . i) = z9 . j ) )
;
then reconsider z =
z as
Function ;
A22:
dom z =
dom (Carrier (OAF,Pa))
by A21, CARD_3:9
.=
the
carrier of
P
by PARTFUN1:def 2
;
rng z c= |.OAF.|
proof
let p be
set ;
TARSKI:def 3 ( not p in rng z or p in |.OAF.| )
assume
p in rng z
;
p in |.OAF.|
then consider r being
set such that A23:
r in dom z
and A24:
z . r = p
by FUNCT_1:def 3;
reconsider r9 =
r as
Element of
P by A22, A23;
reconsider r9 =
r9 as
Element of
P ;
r9 in the
carrier of
P
;
then A25:
ex
U0 being
MSAlgebra of
S st
(
U0 = OAF . r &
(Carrier (OAF,Pa)) . r = the
Sorts of
U0 . Pa )
by PRALG_2:def 9;
|.(OAF . r9).| in { |.(OAF . k).| where k is Element of P : verum }
;
then
|.(OAF . r9).| c= union { |.(OAF . k).| where k is Element of P : verum }
by ZFMISC_1:74;
then A26:
|.(OAF . r9).| c= |.OAF.|
by PRALG_2:def 7;
dom the
Sorts of
(OAF . r9) = the
carrier of
S
by PARTFUN1:def 2;
then A27:
the
Sorts of
(OAF . r9) . Pa in rng the
Sorts of
(OAF . r9)
by FUNCT_1:def 3;
dom z = dom (Carrier (OAF,Pa))
by A21, CARD_3:9;
then
p in (Carrier (OAF,Pa)) . r
by A21, A23, A24, CARD_3:9;
then
p in union (rng the Sorts of (OAF . r9))
by A25, A27, TARSKI:def 4;
then
p in |.(OAF . r9).|
by PRALG_2:def 6;
hence
p in |.OAF.|
by A26;
verum
end;
hence
z in Funcs ( the
carrier of
P,
|.OAF.|)
by A22, FUNCT_2:def 2;
verum
end;
then A28:
y in Funcs (
(Seg (len (the_arity_of o))),
(Funcs ( the carrier of P,|.OAF.|)))
by A17, FUNCT_2:def 2;
per cases
( the_arity_of o <> {} or the_arity_of o = {} )
;
suppose A29:
the_arity_of o <> {}
;
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . jA30:
for
t being
set st
t in dom (doms (OAF ?. o)) holds
Co . t in (doms (OAF ?. o)) . t
proof
let t be
set ;
( t in dom (doms (OAF ?. o)) implies Co . t in (doms (OAF ?. o)) . t )
assume
t in dom (doms (OAF ?. o))
;
Co . t in (doms (OAF ?. o)) . t
then reconsider t =
t as
Element of
P by PRALG_2:11;
reconsider yt =
Co . t as
Function ;
dom (the_arity_of o) <> {}
by A29;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
Co in Funcs ( the
carrier of
P,
(Funcs ((Seg (len (the_arity_of o))),|.OAF.|)))
by A28, FUNCT_6:55;
then A31:
ex
ss being
Function st
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (
(Seg (len (the_arity_of o))),
|.OAF.|) )
by FUNCT_2:def 2;
A32:
Co . t in product ( the Sorts of (OAF . t) * (the_arity_of o))
proof
A33:
dom ( the Sorts of (OAF . t) * (the_arity_of o)) =
dom (the_arity_of o)
by PRALG_2:3
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
A34:
dom y = Seg (len (the_arity_of o))
by A16, FINSEQ_1:def 3;
A35:
for
w being
set st
w in dom ( the Sorts of (OAF . t) * (the_arity_of o)) holds
yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w
proof
dom (the_arity_of o) <> {}
by A29;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then A36:
y = commute (commute y)
by A28, FUNCT_6:57;
let w be
set ;
( w in dom ( the Sorts of (OAF . t) * (the_arity_of o)) implies yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w )
reconsider Pi =
(the_arity_of o) /. w as
SortSymbol of
S ;
A37:
dom (Carrier (OAF,((the_arity_of o) /. w))) = the
carrier of
P
by PARTFUN1:def 2;
assume A38:
w in dom ( the Sorts of (OAF . t) * (the_arity_of o))
;
yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w
then A39:
w in dom (the_arity_of o)
by A33, FINSEQ_1:def 3;
y . w in (MS * (the_arity_of o)) . w
by A8, A14, A33, A34, A38, CARD_3:9;
then A40:
y . w in MS . ((the_arity_of o) . w)
by A39, FUNCT_1:13;
reconsider y =
y as
Function-yielding Function by A36;
reconsider yw =
y . w as
Function ;
y . w in MS . ((the_arity_of o) /. w)
by A39, A40, PARTFUN1:def 6;
then
yw in { ff where ff is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (ff . i) = ff . j }
by A1;
then
ex
jg being
Element of
product (Carrier (OAF,Pi)) st
(
jg = yw & ( for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . Pi) . (jg . i) = jg . j ) )
;
then A41:
yw . t in (Carrier (OAF,((the_arity_of o) /. w))) . t
by A37, CARD_3:9;
ex
U0 being
MSAlgebra of
S st
(
U0 = OAF . t &
(Carrier (OAF,((the_arity_of o) /. w))) . t = the
Sorts of
U0 . ((the_arity_of o) /. w) )
by PRALG_2:def 9;
then (Carrier (OAF,((the_arity_of o) /. w))) . t =
the
Sorts of
(OAF . t) . ((the_arity_of o) . w)
by A39, PARTFUN1:def 6
.=
( the Sorts of (OAF . t) * (the_arity_of o)) . w
by A39, FUNCT_1:13
;
hence
yt . w in ( the Sorts of (OAF . t) * (the_arity_of o)) . w
by A28, A33, A38, A41, FUNCT_6:56;
verum
end;
Co . t in rng Co
by A31, FUNCT_1:def 3;
then
ex
ts being
Function st
(
ts = Co . t &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A31, FUNCT_2:def 2;
hence
Co . t in product ( the Sorts of (OAF . t) * (the_arity_of o))
by A33, A35, CARD_3:9;
verum
end;
(doms (OAF ?. o)) . t = Args (
o,
(OAF . t))
by PRALG_2:11;
hence
Co . t in (doms (OAF ?. o)) . t
by A32, PRALG_2:3;
verum
end; A42:
Co in product (doms (OAF ?. o))
A43:
OPE = IFEQ (
(the_arity_of o),
{},
(commute (OAF ?. o)),
(Commute (Frege (OAF ?. o))))
by PRALG_2:def 13;
then A44:
y in dom (Commute (Frege (OAF ?. o)))
by A11, A12, A29, FUNCOP_1:def 8;
reconsider y1 =
(commute y) . i as
Function ;
A45:
dom (OAF ?. o) = the
carrier of
P
by PARTFUN1:def 2;
A46:
x1 =
OPE . y
by A5, A6, A12, FUNCT_1:47
.=
(Commute (Frege (OAF ?. o))) . y
by A29, A43, FUNCOP_1:def 8
.=
(Frege (OAF ?. o)) . (commute y)
by A44, PRALG_2:def 1
.=
(OAF ?. o) .. (commute y)
by A42, PRALG_2:def 2
;
then A47:
x1 . i =
((OAF ?. o) . i) . ((commute y) . i)
by A45, PRALG_1:def 17
.=
(Den (o,(OAF . i))) . y1
by PRALG_2:7
;
dom (the_arity_of o) <> {}
by A29;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
Co in Funcs ( the
carrier of
P,
(Funcs ((Seg (len (the_arity_of o))),|.OAF.|)))
by A28, FUNCT_6:55;
then A48:
ex
ss being
Function st
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (
(Seg (len (the_arity_of o))),
|.OAF.|) )
by FUNCT_2:def 2;
y1 in product ( the Sorts of (OAF . i) * (the_arity_of o))
proof
A49:
dom ( the Sorts of (OAF . i) * (the_arity_of o)) =
dom (the_arity_of o)
by PRALG_2:3
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
A50:
for
w being
set st
w in dom ( the Sorts of (OAF . i) * (the_arity_of o)) holds
y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w
proof
dom (the_arity_of o) <> {}
by A29;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then A51:
y = commute (commute y)
by A28, FUNCT_6:57;
let w be
set ;
( w in dom ( the Sorts of (OAF . i) * (the_arity_of o)) implies y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w )
reconsider Pi =
(the_arity_of o) /. w as
SortSymbol of
S ;
A52:
dom (Carrier (OAF,((the_arity_of o) /. w))) = the
carrier of
P
by PARTFUN1:def 2;
assume A53:
w in dom ( the Sorts of (OAF . i) * (the_arity_of o))
;
y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w
then A54:
w in dom (the_arity_of o)
by A49, FINSEQ_1:def 3;
w in dom y
by A16, A49, A53, FINSEQ_1:def 3;
then
y . w in (MS * (the_arity_of o)) . w
by A8, A14, CARD_3:9;
then A55:
y . w in MS . ((the_arity_of o) . w)
by A54, FUNCT_1:13;
reconsider y =
y as
Function-yielding Function by A51;
reconsider yw =
y . w as
Function ;
y . w in MS . ((the_arity_of o) /. w)
by A54, A55, PARTFUN1:def 6;
then
yw in { ff where ff is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (ff . i) = ff . j }
by A1;
then
ex
jg being
Element of
product (Carrier (OAF,Pi)) st
(
jg = yw & ( for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . Pi) . (jg . i) = jg . j ) )
;
then A56:
yw . i in (Carrier (OAF,((the_arity_of o) /. w))) . i
by A52, CARD_3:9;
ex
U0 being
MSAlgebra of
S st
(
U0 = OAF . i &
(Carrier (OAF,((the_arity_of o) /. w))) . i = the
Sorts of
U0 . ((the_arity_of o) /. w) )
by PRALG_2:def 9;
then (Carrier (OAF,((the_arity_of o) /. w))) . i =
the
Sorts of
(OAF . i) . ((the_arity_of o) . w)
by A54, PARTFUN1:def 6
.=
( the Sorts of (OAF . i) * (the_arity_of o)) . w
by A54, FUNCT_1:13
;
hence
y1 . w in ( the Sorts of (OAF . i) * (the_arity_of o)) . w
by A28, A49, A53, A56, FUNCT_6:56;
verum
end;
Co . i in rng Co
by A48, FUNCT_1:def 3;
then
ex
ts being
Function st
(
ts = Co . i &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A48, FUNCT_2:def 2;
hence
y1 in product ( the Sorts of (OAF . i) * (the_arity_of o))
by A49, A50, CARD_3:9;
verum
end; then reconsider y19 =
y1 as
Element of
Args (
o,
(OAF . i))
by PRALG_2:3;
A57:
bind (
B,
i,
j)
is_homomorphism OAF . i,
OAF . j
by A13, Th2;
(bind (B,i,j)) # y19 = (commute y) . j
proof
A58:
dom ((bind (B,i,j)) # y19) =
dom (the_arity_of o)
by MSUALG_3:6
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
then reconsider One =
(bind (B,i,j)) # y19 as
FinSequence by FINSEQ_1:def 2;
dom (the_arity_of o) <> {}
by A29;
then A59:
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
y = commute (commute y)
by A28, FUNCT_6:57;
then reconsider y =
y as
Function-yielding Function ;
reconsider y2 =
(commute y) . j as
Function ;
Co in Funcs ( the
carrier of
P,
(Funcs ((Seg (len (the_arity_of o))),|.OAF.|)))
by A28, A59, FUNCT_6:55;
then A60:
ex
ss being
Function st
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (
(Seg (len (the_arity_of o))),
|.OAF.|) )
by FUNCT_2:def 2;
then
Co . j in rng Co
by FUNCT_1:def 3;
then A61:
ex
ts being
Function st
(
ts = Co . j &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A60, FUNCT_2:def 2;
then reconsider Two =
y2 as
FinSequence by FINSEQ_1:def 2;
A62:
Co . i in rng Co
by A60, FUNCT_1:def 3;
now let n be
Nat;
( n in dom y2 implies ((bind (B,i,j)) # y19) . n = y2 . n )reconsider yn =
y . n as
Function ;
reconsider Pi =
(the_arity_of o) /. n as
SortSymbol of
S ;
A63:
ex
ts9 being
Function st
(
ts9 = Co . i &
dom ts9 = Seg (len (the_arity_of o)) &
rng ts9 c= |.OAF.| )
by A60, A62, FUNCT_2:def 2;
assume A64:
n in dom y2
;
((bind (B,i,j)) # y19) . n = y2 . nthen A65:
y . n in (MS * (the_arity_of o)) . n
by A8, A14, A17, A61, CARD_3:9;
A66:
n in dom (the_arity_of o)
by A61, A64, FINSEQ_1:def 3;
then
(the_arity_of o) /. n = (the_arity_of o) . n
by PARTFUN1:def 6;
then
yn in MS . Pi
by A66, A65, FUNCT_1:13;
then
yn in { f where f is Element of product (Carrier (OAF,Pi)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . Pi) . (f . i) = f . j }
by A1;
then A67:
ex
yn9 being
Element of
product (Carrier (OAF,Pi)) st
(
yn9 = yn & ( for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . Pi) . (yn9 . i) = yn9 . j ) )
;
y19 . n = yn . i
by A28, A61, A64, FUNCT_6:56;
then ((bind (B,i,j)) # y19) . n =
((bind (B,i,j)) . ((the_arity_of o) /. n)) . (yn . i)
by A61, A64, A63, MSUALG_3:def 6
.=
yn . j
by A13, A67
;
hence
((bind (B,i,j)) # y19) . n = y2 . n
by A28, A61, A64, FUNCT_6:56;
verum end;
then
for
n being
Nat st
n in Seg (len (the_arity_of o)) holds
One . n = Two . n
by A61;
hence
(bind (B,i,j)) # y19 = (commute y) . j
by A61, A58, FINSEQ_1:13;
verum
end; then (Den (o,(OAF . j))) . ((bind (B,i,j)) # y19) =
((OAF ?. o) . j) . ((commute y) . j)
by PRALG_2:7
.=
x1 . j
by A45, A46, PRALG_1:def 17
;
hence
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
by A57, A47, MSUALG_3:def 7;
verum end; suppose A68:
the_arity_of o = {}
;
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . jreconsider co =
(commute (OAF ?. o)) . y as
Function ;
A69:
MS * {} = {}
;
A70:
co = (curry' (uncurry (OAF ?. o))) . y
by FUNCT_6:def 10;
A71:
dom (OAF ?. o) = the
carrier of
P
by PARTFUN1:def 2;
A72:
Den (
o,
(product OAF)) =
the
Charact of
(product OAF) . o
by MSUALG_1:def 6
.=
(OPS OAF) . o
by PRALG_2:12
.=
IFEQ (
(the_arity_of o),
{},
(commute (OAF ?. o)),
(Commute (Frege (OAF ?. o))))
by PRALG_2:def 13
.=
commute (OAF ?. o)
by A68, FUNCOP_1:def 8
;
A73:
for
d being
Element of
P holds
x1 . d = (Den (o,(OAF . d))) . {}
proof
reconsider co9 =
(curry' (uncurry (OAF ?. o))) . y as
Function by A70;
let d be
Element of
P;
x1 . d = (Den (o,(OAF . d))) . {}
reconsider g =
(OAF ?. o) . d as
Function ;
A74:
x1 = (commute (OAF ?. o)) . y
by A5, A6, A72, FUNCT_1:47;
g = Den (
o,
(OAF . d))
by PRALG_2:7;
then dom g =
Args (
o,
(OAF . d))
by FUNCT_2:def 1
.=
{{}}
by A68, PRALG_2:4
;
then A75:
y in dom g
by A8, A68, CARD_3:10;
then A76:
[d,y] in dom (uncurry (OAF ?. o))
by A71, FUNCT_5:38;
co . d =
co9 . d
by FUNCT_6:def 10
.=
(uncurry (OAF ?. o)) . (
d,
y)
by A76, FUNCT_5:22
.=
g . y
by A71, A75, FUNCT_5:38
;
then x1 . d =
(Den (o,(OAF . d))) . y
by A74, PRALG_2:7
.=
(Den (o,(OAF . d))) . {}
by A8, A68, A69, CARD_3:10, TARSKI:def 1
;
hence
x1 . d = (Den (o,(OAF . d))) . {}
;
verum
end; then A77:
x1 . i = (Den (o,(OAF . i))) . {}
;
Args (
o,
(OAF . i))
= {{}}
by A68, PRALG_2:4;
then reconsider E =
{} as
Element of
Args (
o,
(OAF . i))
by TARSKI:def 1;
set F =
bind (
B,
i,
j);
A78:
Args (
o,
(OAF . j))
= {{}}
by A68, PRALG_2:4;
bind (
B,
i,
j)
is_homomorphism OAF . i,
OAF . j
by A13, Th2;
then A79:
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = (Den (o,(OAF . j))) . ((bind (B,i,j)) # E)
by A77, MSUALG_3:def 7;
x1 . j = (Den (o,(OAF . j))) . {}
by A73;
hence
((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j
by A79, A78, TARSKI:def 1;
verum end;
end; then
x in { f where f is Element of product (Carrier (OAF,(the_result_sort_of o))) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . (the_result_sort_of o)) . (f . i) = f . j }
by A10;
hence
x in C . (the_result_sort_of o)
by A1;
verum end;
then
x in C . (the_result_sort_of o)
;
then A80:
x in C . ( the ResultSort of S . o)
by MSUALG_1:def 2;
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
hence
x in (C * the ResultSort of S) . o
by A80, FUNCT_1:13;
verum
end;
hence
C is_closed_on o
by MSUALG_2:def 5;
verum
end;
then A81:
C is opers_closed
by MSUALG_2:def 6;
reconsider C = C as MSSubset of L ;
set MSA = L | C;
A82:
L | C = MSAlgebra(# C,(Opers (L,C)) #)
by A81, MSUALG_2:def 15;
now let s be
SortSymbol of
S;
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of (L | C) . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )let f be
Element of
(SORTS OAF) . s;
( f in the Sorts of (L | C) . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )A83:
f is
Element of
product (Carrier (OAF,s))
by PRALG_2:def 10;
thus
(
f in the
Sorts of
(L | C) . s iff for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
verumproof
hereby ( ( for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) implies f in the Sorts of (L | C) . s )
assume
f in the
Sorts of
(L | C) . s
;
for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . jthen
f in { g where g is Element of product (Carrier (OAF,s)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (g . i) = g . j }
by A1, A82;
then
ex
k being
Element of
product (Carrier (OAF,s)) st
(
k = f & ( for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . s) . (k . i) = k . j ) )
;
hence
for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j
;
verum
end;
assume
for
i,
j being
Element of
P st
i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j
;
f in the Sorts of (L | C) . s
then
f in { h where h is Element of product (Carrier (OAF,s)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (h . i) = h . j }
by A83;
hence
f in the
Sorts of
(L | C) . s
by A1, A82;
verum
end; end;
hence
ex b1 being strict MSSubAlgebra of product OAF st
for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b1 . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j )
; verum