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 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 5;
then reconsider C = C as ManySortedSubset of SORTS OAF by PBOOLE:def 23;
reconsider C = C as MSSubset of (product OAF) by PRALG_2:20;
for o being OperSymbol of S holds C is_closed_on o
proof
let o be
OperSymbol of
S;
:: thesis: C is_closed_on o
rng ((Den o,(product OAF)) | (((C # ) * the Arity of S) . o)) c= (C * the ResultSort of S) . o
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng ((Den o,(product OAF)) | (((C # ) * the Arity of S) . o)) or x in (C * the ResultSort of S) . o )
assume A3:
x in rng ((Den o,(product OAF)) | (((C # ) * the Arity of S) . o))
;
:: thesis: x in (C * the ResultSort of S) . o
reconsider K =
(Den o,(product OAF)) | (((C # ) * the Arity of S) . o) as
Function ;
consider y being
set such that A4:
(
y in dom K &
x = K . y )
by A3, FUNCT_1:def 5;
dom K = (dom (Den o,(product OAF))) /\ (((C # ) * the Arity of S) . o)
by RELAT_1:90;
then A5:
(
y in dom (Den o,(product OAF)) &
y in ((C # ) * the Arity of S) . o )
by A4, XBOOLE_0:def 4;
reconsider MS =
C as
ManySortedSet of ;
dom the
Arity of
S = the
carrier' of
S
by FUNCT_2:def 1;
then
y in (C # ) . (the Arity of S . o)
by A5, FUNCT_1:23;
then
y in (C # ) . (the_arity_of o)
by MSUALG_1:def 6;
then A7:
y in product (MS * (the_arity_of o))
by PBOOLE:def 19;
A8:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
x in Result o,
(product OAF)
by A3;
then
x in (the Sorts of (product OAF) * the ResultSort of S) . o
by MSUALG_1:def 10;
then
x in the
Sorts of
(product OAF) . (the ResultSort of S . o)
by A8, FUNCT_1:23;
then
x in (SORTS OAF) . (the ResultSort of S . o)
by PRALG_2:20;
then
x in (SORTS OAF) . (the_result_sort_of o)
by MSUALG_1:def 7;
then A9:
x is
Element of
product (Carrier OAF,(the_result_sort_of o))
by PRALG_2:def 17;
then reconsider x1 =
x as
Function ;
now let s be
SortSymbol of
S;
:: thesis: 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
let i,
j be
Element of
P;
:: thesis: ( i >= j implies ((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . j )
assume A10:
i >= j
;
:: thesis: ((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . j
A11:
Den o,
(product OAF) =
the
Charact of
(product OAF) . o
by MSUALG_1:def 11
.=
(OPS OAF) . o
by PRALG_2:20
;
reconsider OPE =
(OPS OAF) . o as
Function ;
consider g being
Function such that A12:
(
y = g &
dom g = dom (MS * (the_arity_of o)) & ( for
t being
set st
t in dom (MS * (the_arity_of o)) holds
g . t in (MS * (the_arity_of o)) . t ) )
by A7, CARD_3:def 5;
reconsider y =
y as
Function by A12;
A13:
dom y = dom (MS * (the_arity_of o))
by A7, CARD_3:18;
A14:
rng (the_arity_of o) c= dom MS
then A15:
dom y = dom (the_arity_of o)
by A13, RELAT_1:46;
set y1 =
(commute y) . i;
reconsider Co =
commute y as
Function ;
A16:
y in Funcs (Seg (len (the_arity_of o))),
(Funcs the carrier of P,|.OAF.|)
proof
A17:
dom y = Seg (len (the_arity_of o))
by A15, FINSEQ_1:def 3;
rng y c= Funcs the
carrier of
P,
|.OAF.|
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in rng y or z in Funcs the carrier of P,|.OAF.| )
assume
z in rng y
;
:: thesis: z in Funcs the carrier of P,|.OAF.|
then consider n being
set such that A18:
(
n in dom y &
z = y . n )
by FUNCT_1:def 5;
A19:
n in dom (MS * (the_arity_of o))
by A7, A18, CARD_3:18;
then
z in (MS * (the_arity_of o)) . n
by A7, A18, CARD_3:18;
then A20:
z in MS . ((the_arity_of o) . n)
by A19, FUNCT_1:22;
n in dom (the_arity_of o)
by A14, A19, RELAT_1:46;
then
(the_arity_of o) . n = (the_arity_of o) /. n
by PARTFUN1:def 8;
then reconsider Pa =
(the_arity_of o) . n as
SortSymbol of
S ;
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, A20;
then consider z' being
Element of
product (Carrier OAF,Pa) such that A21:
(
z' = z & ( for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . Pa) . (z' . i) = z' . j ) )
;
reconsider z =
z as
Function by A21;
A22:
dom z =
dom (Carrier OAF,Pa)
by A21, CARD_3:18
.=
the
carrier of
P
by PARTFUN1:def 4
;
rng z c= |.OAF.|
hence
z in Funcs the
carrier of
P,
|.OAF.|
by A22, FUNCT_2:def 2;
:: thesis: verum
end;
hence
y in Funcs (Seg (len (the_arity_of o))),
(Funcs the carrier of P,|.OAF.|)
by A17, FUNCT_2:def 2;
:: thesis: verum
end;
per cases
( the_arity_of o <> {} or the_arity_of o = {} )
;
suppose A27:
the_arity_of o <> {}
;
:: thesis: ((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . jthen
dom (the_arity_of o) <> {}
;
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 A16, FUNCT_6:85;
then consider ss being
Function such that A28:
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (Seg (len (the_arity_of o))),
|.OAF.| )
by FUNCT_2:def 2;
reconsider y1 =
(commute y) . i as
Function ;
A29:
y1 in product (the Sorts of (OAF . i) * (the_arity_of o))
proof
A30:
dom (the Sorts of (OAF . i) * (the_arity_of o)) =
dom (the_arity_of o)
by PRALG_2:10
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
Co . i in rng Co
by A28, FUNCT_1:def 5;
then consider ts being
Function such that A31:
(
ts = Co . i &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A28, FUNCT_2:def 2;
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
let w be
set ;
:: thesis: ( 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 )
assume A32:
w in dom (the Sorts of (OAF . i) * (the_arity_of o))
;
:: thesis: y1 . w in (the Sorts of (OAF . i) * (the_arity_of o)) . w
then A33:
w in dom y
by A15, A30, FINSEQ_1:def 3;
A34:
w in dom (the_arity_of o)
by A30, A32, FINSEQ_1:def 3;
y . w in (MS * (the_arity_of o)) . w
by A7, A13, A33, CARD_3:18;
then A35:
y . w in MS . ((the_arity_of o) . w)
by A34, FUNCT_1:23;
dom (the_arity_of o) <> {}
by A27;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
y = commute (commute y)
by A16, FUNCT_6:87;
then reconsider y =
y as
Function-yielding Function ;
A36:
y . w in MS . ((the_arity_of o) /. w)
by A34, A35, PARTFUN1:def 8;
reconsider yw =
y . w as
Function ;
reconsider Pi =
(the_arity_of o) /. w as
SortSymbol of
S ;
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, A36;
then consider jg being
Element of
product (Carrier OAF,Pi) such that A37:
(
jg = yw & ( for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . Pi) . (jg . i) = jg . j ) )
;
dom (Carrier OAF,((the_arity_of o) /. w)) = the
carrier of
P
by PARTFUN1:def 4;
then A38:
yw . i in (Carrier OAF,((the_arity_of o) /. w)) . i
by A37, CARD_3:18;
consider U0 being
MSAlgebra of
S such that A39:
(
U0 = OAF . i &
(Carrier OAF,((the_arity_of o) /. w)) . i = the
Sorts of
U0 . ((the_arity_of o) /. w) )
by PRALG_2:def 16;
(Carrier OAF,((the_arity_of o) /. w)) . i =
the
Sorts of
(OAF . i) . ((the_arity_of o) . w)
by A34, A39, PARTFUN1:def 8
.=
(the Sorts of (OAF . i) * (the_arity_of o)) . w
by A34, FUNCT_1:23
;
hence
y1 . w in (the Sorts of (OAF . i) * (the_arity_of o)) . w
by A16, A30, A32, A38, FUNCT_6:86;
:: thesis: verum
end;
hence
y1 in product (the Sorts of (OAF . i) * (the_arity_of o))
by A30, A31, CARD_3:18;
:: thesis: verum
end; A40:
for
t being
set st
t in dom (doms (OAF ?. o)) holds
Co . t in (doms (OAF ?. o)) . t
proof
let t be
set ;
:: thesis: ( t in dom (doms (OAF ?. o)) implies Co . t in (doms (OAF ?. o)) . t )
assume
t in dom (doms (OAF ?. o))
;
:: thesis: Co . t in (doms (OAF ?. o)) . t
then reconsider t =
t as
Element of
P by PRALG_2:18;
A41:
(doms (OAF ?. o)) . t = Args o,
(OAF . t)
by PRALG_2:18;
dom (the_arity_of o) <> {}
by A27;
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 A16, FUNCT_6:85;
then consider ss being
Function such that A42:
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (Seg (len (the_arity_of o))),
|.OAF.| )
by FUNCT_2:def 2;
reconsider yt =
Co . t as
Function ;
Co . t in product (the Sorts of (OAF . t) * (the_arity_of o))
proof
A43:
dom (the Sorts of (OAF . t) * (the_arity_of o)) =
dom (the_arity_of o)
by PRALG_2:10
.=
Seg (len (the_arity_of o))
by FINSEQ_1:def 3
;
Co . t in rng Co
by A42, FUNCT_1:def 5;
then consider ts being
Function such that A44:
(
ts = Co . t &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A42, FUNCT_2:def 2;
A45:
dom y = Seg (len (the_arity_of o))
by A15, FINSEQ_1:def 3;
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
let w be
set ;
:: thesis: ( 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 )
assume A46:
w in dom (the Sorts of (OAF . t) * (the_arity_of o))
;
:: thesis: yt . w in (the Sorts of (OAF . t) * (the_arity_of o)) . w
then A47:
w in dom (the_arity_of o)
by A43, FINSEQ_1:def 3;
y . w in (MS * (the_arity_of o)) . w
by A7, A13, A43, A45, A46, CARD_3:18;
then A48:
y . w in MS . ((the_arity_of o) . w)
by A47, FUNCT_1:23;
dom (the_arity_of o) <> {}
by A27;
then
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
y = commute (commute y)
by A16, FUNCT_6:87;
then reconsider y =
y as
Function-yielding Function ;
A49:
y . w in MS . ((the_arity_of o) /. w)
by A47, A48, PARTFUN1:def 8;
reconsider yw =
y . w as
Function ;
reconsider Pi =
(the_arity_of o) /. w as
SortSymbol of
S ;
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, A49;
then consider jg being
Element of
product (Carrier OAF,Pi) such that A50:
(
jg = yw & ( for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . Pi) . (jg . i) = jg . j ) )
;
dom (Carrier OAF,((the_arity_of o) /. w)) = the
carrier of
P
by PARTFUN1:def 4;
then A51:
yw . t in (Carrier OAF,((the_arity_of o) /. w)) . t
by A50, CARD_3:18;
consider U0 being
MSAlgebra of
S such that A52:
(
U0 = OAF . t &
(Carrier OAF,((the_arity_of o) /. w)) . t = the
Sorts of
U0 . ((the_arity_of o) /. w) )
by PRALG_2:def 16;
(Carrier OAF,((the_arity_of o) /. w)) . t =
the
Sorts of
(OAF . t) . ((the_arity_of o) . w)
by A47, A52, PARTFUN1:def 8
.=
(the Sorts of (OAF . t) * (the_arity_of o)) . w
by A47, FUNCT_1:23
;
hence
yt . w in (the Sorts of (OAF . t) * (the_arity_of o)) . w
by A16, A43, A46, A51, FUNCT_6:86;
:: thesis: verum
end;
hence
Co . t in product (the Sorts of (OAF . t) * (the_arity_of o))
by A43, A44, CARD_3:18;
:: thesis: verum
end;
hence
Co . t in (doms (OAF ?. o)) . t
by A41, PRALG_2:10;
:: thesis: verum
end; A53:
Co in product (doms (OAF ?. o))
reconsider y1' =
y1 as
Element of
Args o,
(OAF . i) by A29, PRALG_2:10;
A55:
dom (OAF ?. o) = the
carrier of
P
by PARTFUN1:def 4;
A56:
bind B,
i,
j is_homomorphism OAF . i,
OAF . j
by A10, Th2;
A57:
OPE = IFEQ (the_arity_of o),
{} ,
(commute (OAF ?. o)),
(Commute (Frege (OAF ?. o)))
by PRALG_2:def 20;
then A58:
y in dom (Commute (Frege (OAF ?. o)))
by A5, A11, A27, FUNCOP_1:def 8;
A59:
x1 =
OPE . y
by A4, A11, FUNCT_1:70
.=
(Commute (Frege (OAF ?. o))) . y
by A27, A57, FUNCOP_1:def 8
.=
(Frege (OAF ?. o)) . (commute y)
by A58, PRALG_2:def 6
.=
(OAF ?. o) .. (commute y)
by A53, PRALG_2:def 8
;
then A60:
x1 . i =
((OAF ?. o) . i) . ((commute y) . i)
by A55, PRALG_1:def 17
.=
(Den o,(OAF . i)) . y1
by PRALG_2:14
;
(bind B,i,j) # y1' = (commute y) . j
proof
dom (the_arity_of o) <> {}
by A27;
then A61:
Seg (len (the_arity_of o)) <> {}
by FINSEQ_1:def 3;
then
y = commute (commute y)
by A16, FUNCT_6:87;
then reconsider y =
y as
Function-yielding Function ;
Co in Funcs the
carrier of
P,
(Funcs (Seg (len (the_arity_of o))),|.OAF.|)
by A16, A61, FUNCT_6:85;
then consider ss being
Function such that A62:
(
ss = Co &
dom ss = the
carrier of
P &
rng ss c= Funcs (Seg (len (the_arity_of o))),
|.OAF.| )
by FUNCT_2:def 2;
reconsider y2 =
(commute y) . j as
Function ;
A63:
Co . j in rng Co
by A62, FUNCT_1:def 5;
A64:
Co . i in rng Co
by A62, FUNCT_1:def 5;
consider ts being
Function such that A65:
(
ts = Co . j &
dom ts = Seg (len (the_arity_of o)) &
rng ts c= |.OAF.| )
by A62, A63, FUNCT_2:def 2;
reconsider Two =
y2 as
FinSequence by A65, FINSEQ_1:def 2;
A66:
now let n be
Nat;
:: thesis: ( n in dom y2 implies ((bind B,i,j) # y1') . n = y2 . n )assume A67:
n in dom y2
;
:: thesis: ((bind B,i,j) # y1') . n = y2 . nthen A68:
n in dom (the_arity_of o)
by A65, FINSEQ_1:def 3;
consider ts' being
Function such that A69:
(
ts' = Co . i &
dom ts' = Seg (len (the_arity_of o)) &
rng ts' c= |.OAF.| )
by A62, A64, FUNCT_2:def 2;
consider sT being
Function such that A70:
(
sT = y &
dom sT = Seg (len (the_arity_of o)) &
rng sT c= Funcs the
carrier of
P,
|.OAF.| )
by A16, FUNCT_2:def 2;
reconsider yn =
y . n as
Function ;
A71:
y1' . n = yn . i
by A16, A65, A67, FUNCT_6:86;
reconsider Pi =
(the_arity_of o) /. n as
SortSymbol of
S ;
A72:
(the_arity_of o) /. n = (the_arity_of o) . n
by A68, PARTFUN1:def 8;
y . n in (MS * (the_arity_of o)) . n
by A7, A13, A65, A67, A70, CARD_3:18;
then
yn in MS . Pi
by A68, A72, FUNCT_1:23;
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 consider yn' being
Element of
product (Carrier OAF,Pi) such that A73:
(
yn' = yn & ( for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . Pi) . (yn' . i) = yn' . j ) )
;
hence
((bind B,i,j) # y1') . n = y2 . n
by A16, A65, A67, FUNCT_6:86;
:: thesis: verum end;
A74:
dom ((bind B,i,j) # y1') =
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) # y1' as
FinSequence by FINSEQ_1:def 2;
for
n being
Nat st
n in Seg (len (the_arity_of o)) holds
One . n = Two . n
by A65, A66;
hence
(bind B,i,j) # y1' = (commute y) . j
by A65, A74, FINSEQ_1:17;
:: thesis: verum
end; then (Den o,(OAF . j)) . ((bind B,i,j) # y1') =
((OAF ?. o) . j) . ((commute y) . j)
by PRALG_2:14
.=
x1 . j
by A55, A59, PRALG_1:def 17
;
hence
((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . j
by A56, A60, MSUALG_3:def 9;
:: thesis: verum end; suppose A75:
the_arity_of o = {}
;
:: thesis: ((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . jA76:
Den o,
(product OAF) =
the
Charact of
(product OAF) . o
by MSUALG_1:def 11
.=
(OPS OAF) . o
by PRALG_2:20
.=
IFEQ (the_arity_of o),
{} ,
(commute (OAF ?. o)),
(Commute (Frege (OAF ?. o)))
by PRALG_2:def 20
.=
commute (OAF ?. o)
by A75, FUNCOP_1:def 8
;
A77:
MS * {} = {}
;
reconsider co =
(commute (OAF ?. o)) . y as
Function ;
A78:
co = (curry' (uncurry (OAF ?. o))) . y
by FUNCT_6:def 12;
A79:
dom (OAF ?. o) = the
carrier of
P
by PARTFUN1:def 4;
A80:
for
d being
Element of
P holds
x1 . d = (Den o,(OAF . d)) . {}
proof
let d be
Element of
P;
:: thesis: x1 . d = (Den o,(OAF . d)) . {}
reconsider g =
(OAF ?. o) . d as
Function ;
g = Den o,
(OAF . d)
by PRALG_2:14;
then dom g =
Args o,
(OAF . d)
by FUNCT_2:def 1
.=
{{} }
by A75, PRALG_2:11
;
then A81:
y in dom g
by A7, A75, CARD_3:19;
then A82:
[d,y] in dom (uncurry (OAF ?. o))
by A79, FUNCT_5:45;
reconsider co' =
(curry' (uncurry (OAF ?. o))) . y as
Function by A78;
A83:
co . d =
co' . d
by FUNCT_6:def 12
.=
(uncurry (OAF ?. o)) . d,
y
by A82, FUNCT_5:29
.=
g . y
by A79, A81, FUNCT_5:45
;
x1 = (commute (OAF ?. o)) . y
by A4, A76, FUNCT_1:70;
then x1 . d =
(Den o,(OAF . d)) . y
by A83, PRALG_2:14
.=
(Den o,(OAF . d)) . {}
by A7, A75, A77, CARD_3:19, TARSKI:def 1
;
hence
x1 . d = (Den o,(OAF . d)) . {}
;
:: thesis: verum
end; A84:
bind B,
i,
j is_homomorphism OAF . i,
OAF . j
by A10, Th2;
set F =
bind B,
i,
j;
A85:
x1 . i = (Den o,(OAF . i)) . {}
by A80;
A86:
x1 . j = (Den o,(OAF . j)) . {}
by A80;
Args o,
(OAF . i) = {{} }
by A75, PRALG_2:11;
then reconsider E =
{} as
Element of
Args o,
(OAF . i) by TARSKI:def 1;
A87:
((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = (Den o,(OAF . j)) . ((bind B,i,j) # E)
by A84, A85, MSUALG_3:def 9;
Args o,
(OAF . j) = {{} }
by A75, PRALG_2:11;
hence
((bind B,i,j) . (the_result_sort_of o)) . (x1 . i) = x1 . j
by A86, A87, TARSKI:def 1;
:: thesis: 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 A9;
hence
x in C . (the_result_sort_of o)
by A1;
:: thesis: verum end;
then
x in C . (the_result_sort_of o)
;
then A88:
x in C . (the ResultSort of S . o)
by MSUALG_1:def 7;
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
hence
x in (C * the ResultSort of S) . o
by A88, FUNCT_1:23;
:: thesis: verum
end;
hence
C is_closed_on o
by MSUALG_2:def 6;
:: thesis: verum
end;
then A89:
C is opers_closed
by MSUALG_2:def 7;
reconsider L = product OAF as non-empty MSAlgebra of S ;
reconsider C = C as MSSubset of L ;
set MSA = L | C;
A90:
L | C = MSAlgebra(# C,(Opers L,C) #)
by A89, MSUALG_2:def 16;
now let s be
SortSymbol of
S;
:: thesis: 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;
:: thesis: ( 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 )A91:
f is
Element of
product (Carrier OAF,s)
by PRALG_2:def 17;
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 )
:: thesis: verumproof
hereby :: thesis: ( ( 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
;
:: thesis: 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, A90;
then consider k being
Element of
product (Carrier OAF,s) such that A92:
k = f
and A93:
for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . s) . (k . i) = k . j
;
thus
for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . s) . (f . i) = f . j
by A92, A93;
:: thesis: verum
end;
assume
for
i,
j being
Element of
P st
i >= j holds
((bind B,i,j) . s) . (f . i) = f . j
;
:: thesis: 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 A91;
hence
f in the
Sorts of
(L | C) . s
by A1, A90;
:: thesis: 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 )
; :: thesis: verum