reconsider L = product OAF as non-empty MSAlgebra over 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 object st i in the carrier of S holds
C . i c= (SORTS OAF) . i
proof
let i be object ; :: thesis: ( i in the carrier of S implies C . i c= (SORTS OAF) . i )
assume i in the carrier of S ; :: thesis: C . i c= (SORTS OAF) . i
then reconsider s = i as SortSymbol of S ;
defpred S1[ Element of product (Carrier (OAF,s))] means for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (\$1 . i) = \$1 . j;
A2: { f where f is Element of product (Carrier (OAF,s)) : S1[f] } c= product (Carrier (OAF,s)) from (SORTS OAF) . s = product (Carrier (OAF,s)) by PRALG_2:def 10;
hence C . i c= (SORTS OAF) . i by A1, A2; :: thesis: verum
end;
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; :: thesis:
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 object ; :: 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 )
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)) ; :: thesis: x in (C * the ResultSort of S) . o
then consider y being object 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 ;
then y in (C #) . ( the Arity of S . o) by ;
then y in (C #) . () by MSUALG_1:def 1;
then A8: y in product (MS * ()) 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 ;
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) . by ;
then A10: x is Element of product (Carrier (OAF,)) by PRALG_2:def 10;
A11: y in dom (Den (o,(product OAF))) by ;
now :: thesis: for s being SortSymbol of S holds x in C .
let s be SortSymbol of S; :: thesis: x in C .
for i, j being Element of P st i >= j holds
((bind (B,i,j)) . ) . (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; :: thesis: ( i >= j implies ((bind (B,i,j)) . ) . (x1 . i) = x1 . j )
assume A13: i >= j ; :: thesis: ((bind (B,i,j)) . ) . (x1 . i) = x1 . j
reconsider Co = commute y as Function ;
set y1 = () . i;
A14: dom y = dom (MS * ()) by ;
A15: rng () c= dom MS
proof
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng () or i in dom MS )
assume i in rng () ; :: thesis: i in dom MS
then i in the carrier of S ;
hence i in dom MS by PARTFUN1:def 2; :: thesis: verum
end;
then A16: dom y = dom () by ;
then A17: dom y = Seg (len ()) by FINSEQ_1:def 3;
rng y c= Funcs ( the carrier of P,|.OAF.|)
proof
let z be object ; :: 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 object such that
A18: n in dom y and
A19: z = y . n by FUNCT_1:def 3;
A20: n in dom (MS * ()) by ;
then n in dom () by ;
then (the_arity_of o) . n = () /. n by PARTFUN1:def 6;
then reconsider Pa = () . n as SortSymbol of S ;
z in (MS * ()) . n by ;
then z in MS . (() . n) by ;
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
.= the carrier of P by PARTFUN1:def 2 ;
rng z c= |.OAF.|
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in rng z or p in |.OAF.| )
assume p in rng z ; :: thesis: p in |.OAF.|
then consider r being object 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 ;
reconsider r9 = r9 as Element of P ;
r9 in the carrier of P ;
then A25: ex U0 being MSAlgebra over 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 ;
then p in (Carrier (OAF,Pa)) . r by ;
then p in union (rng the Sorts of (OAF . r9)) by ;
then p in |.(OAF . r9).| by PRALG_2:def 6;
hence p in |.OAF.| by A26; :: thesis: verum
end;
hence z in Funcs ( the carrier of P,|.OAF.|) by ; :: thesis: verum
end;
then A28: y in Funcs ((Seg (len ())),(Funcs ( the carrier of P,|.OAF.|))) by ;
per cases ;
suppose A29: the_arity_of o <> {} ; :: thesis: ((bind (B,i,j)) . ) . (x1 . i) = x1 . j
A30: for t being object st t in dom (doms (OAF ?. o)) holds
Co . t in (doms (OAF ?. o)) . t
proof
let t be object ; :: 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:11;
reconsider yt = Co . t as Function ;
dom () <> {} by A29;
then Seg (len ()) <> {} by FINSEQ_1:def 3;
then Co in Funcs ( the carrier of P,(Funcs ((Seg (len ())),|.OAF.|))) by ;
then A31: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len ())),|.OAF.|) ) by FUNCT_2:def 2;
A32: Co . t in product ( the Sorts of (OAF . t) * ())
proof
A33: dom ( the Sorts of (OAF . t) * ()) = dom () by PRALG_2:3
.= Seg (len ()) by FINSEQ_1:def 3 ;
A34: dom y = Seg (len ()) by ;
A35: for w being object st w in dom ( the Sorts of (OAF . t) * ()) holds
yt . w in ( the Sorts of (OAF . t) * ()) . w
proof
dom () <> {} by A29;
then Seg (len ()) <> {} by FINSEQ_1:def 3;
then A36: y = commute () by ;
let w be object ; :: thesis: ( w in dom ( the Sorts of (OAF . t) * ()) implies yt . w in ( the Sorts of (OAF . t) * ()) . w )
reconsider Pi = () /. w as SortSymbol of S ;
A37: dom (Carrier (OAF,(() /. w))) = the carrier of P by PARTFUN1:def 2;
assume A38: w in dom ( the Sorts of (OAF . t) * ()) ; :: thesis: yt . w in ( the Sorts of (OAF . t) * ()) . w
then A39: w in dom () by ;
y . w in (MS * ()) . w by ;
then A40: y . w in MS . (() . w) by ;
reconsider y = y as Function-yielding Function by A36;
reconsider yw = y . w as Function ;
y . w in MS . (() /. w) by ;
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,(() /. w))) . t by ;
ex U0 being MSAlgebra over S st
( U0 = OAF . t & (Carrier (OAF,(() /. w))) . t = the Sorts of U0 . (() /. w) ) by PRALG_2:def 9;
then (Carrier (OAF,(() /. w))) . t = the Sorts of (OAF . t) . (() . w) by
.= ( the Sorts of (OAF . t) * ()) . w by ;
hence yt . w in ( the Sorts of (OAF . t) * ()) . w by ; :: thesis: verum
end;
Co . t in rng Co by ;
then ex ts being Function st
( ts = Co . t & dom ts = Seg (len ()) & rng ts c= |.OAF.| ) by ;
hence Co . t in product ( the Sorts of (OAF . t) * ()) by ; :: thesis: verum
end;
(doms (OAF ?. o)) . t = Args (o,(OAF . t)) by PRALG_2:11;
hence Co . t in (doms (OAF ?. o)) . t by ; :: thesis: verum
end;
A42: Co in product (doms (OAF ?. o))
proof
dom () <> {} by A29;
then Seg (len ()) <> {} by FINSEQ_1:def 3;
then Co in Funcs ( the carrier of P,(Funcs ((Seg (len ())),|.OAF.|))) by ;
then ex Co9 being Function st
( Co9 = Co & dom Co9 = the carrier of P & rng Co9 c= Funcs ((Seg (len ())),|.OAF.|) ) by FUNCT_2:def 2;
then dom Co = dom (doms (OAF ?. o)) by PRALG_2:11;
hence Co in product (doms (OAF ?. o)) by ; :: thesis: verum
end;
A43: OPE = IFEQ ((),{},(commute (OAF ?. o)),(Commute (Frege (OAF ?. o)))) by PRALG_2:def 13;
then A44: y in dom (Commute (Frege (OAF ?. o))) by ;
reconsider y1 = () . i as Function ;
A45: dom (OAF ?. o) = the carrier of P by PARTFUN1:def 2;
A46: x1 = OPE . y by
.= (Commute (Frege (OAF ?. o))) . y by
.= (Frege (OAF ?. o)) . () by
.= (OAF ?. o) .. () by ;
then A47: x1 . i = ((OAF ?. o) . i) . (() . i) by
.= (Den (o,(OAF . i))) . y1 by PRALG_2:7 ;
dom () <> {} by A29;
then Seg (len ()) <> {} by FINSEQ_1:def 3;
then Co in Funcs ( the carrier of P,(Funcs ((Seg (len ())),|.OAF.|))) by ;
then A48: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len ())),|.OAF.|) ) by FUNCT_2:def 2;
y1 in product ( the Sorts of (OAF . i) * ())
proof
A49: dom ( the Sorts of (OAF . i) * ()) = dom () by PRALG_2:3
.= Seg (len ()) by FINSEQ_1:def 3 ;
A50: for w being object st w in dom ( the Sorts of (OAF . i) * ()) holds
y1 . w in ( the Sorts of (OAF . i) * ()) . w
proof
dom () <> {} by A29;
then Seg (len ()) <> {} by FINSEQ_1:def 3;
then A51: y = commute () by ;
let w be object ; :: thesis: ( w in dom ( the Sorts of (OAF . i) * ()) implies y1 . w in ( the Sorts of (OAF . i) * ()) . w )
reconsider Pi = () /. w as SortSymbol of S ;
A52: dom (Carrier (OAF,(() /. w))) = the carrier of P by PARTFUN1:def 2;
assume A53: w in dom ( the Sorts of (OAF . i) * ()) ; :: thesis: y1 . w in ( the Sorts of (OAF . i) * ()) . w
then A54: w in dom () by ;
w in dom y by ;
then y . w in (MS * ()) . w by ;
then A55: y . w in MS . (() . w) by ;
reconsider y = y as Function-yielding Function by A51;
reconsider yw = y . w as Function ;
y . w in MS . (() /. w) by ;
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,(() /. w))) . i by ;
ex U0 being MSAlgebra over S st
( U0 = OAF . i & (Carrier (OAF,(() /. w))) . i = the Sorts of U0 . (() /. w) ) by PRALG_2:def 9;
then (Carrier (OAF,(() /. w))) . i = the Sorts of (OAF . i) . (() . w) by
.= ( the Sorts of (OAF . i) * ()) . w by ;
hence y1 . w in ( the Sorts of (OAF . i) * ()) . w by ; :: thesis: verum
end;
Co . i in rng Co by ;
then ex ts being Function st
( ts = Co . i & dom ts = Seg (len ()) & rng ts c= |.OAF.| ) by ;
hence y1 in product ( the Sorts of (OAF . i) * ()) by ; :: thesis: 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 ;
(bind (B,i,j)) # y19 = () . j
proof
A58: dom ((bind (B,i,j)) # y19) = dom () by MSUALG_3:6
.= Seg (len ()) by FINSEQ_1:def 3 ;
then reconsider One = (bind (B,i,j)) # y19 as FinSequence by FINSEQ_1:def 2;
dom () <> {} by A29;
then A59: Seg (len ()) <> {} by FINSEQ_1:def 3;
then y = commute () by ;
then reconsider y = y as Function-yielding Function ;
reconsider y2 = () . j as Function ;
Co in Funcs ( the carrier of P,(Funcs ((Seg (len ())),|.OAF.|))) by ;
then A60: ex ss being Function st
( ss = Co & dom ss = the carrier of P & rng ss c= Funcs ((Seg (len ())),|.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 ()) & rng ts c= |.OAF.| ) by ;
then reconsider Two = y2 as FinSequence by FINSEQ_1:def 2;
A62: Co . i in rng Co by ;
now :: thesis: for n being Nat st n in dom y2 holds
((bind (B,i,j)) # y19) . n = y2 . n
let n be Nat; :: thesis: ( n in dom y2 implies ((bind (B,i,j)) # y19) . n = y2 . n )
reconsider yn = y . n as Function ;
reconsider Pi = () /. n as SortSymbol of S ;
A63: ex ts9 being Function st
( ts9 = Co . i & dom ts9 = Seg (len ()) & rng ts9 c= |.OAF.| ) by ;
assume A64: n in dom y2 ; :: thesis: ((bind (B,i,j)) # y19) . n = y2 . n
then A65: y . n in (MS * ()) . n by ;
A66: n in dom () by ;
then (the_arity_of o) /. n = () . n by PARTFUN1:def 6;
then yn in MS . Pi by ;
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 ;
then ((bind (B,i,j)) # y19) . n = ((bind (B,i,j)) . (() /. n)) . (yn . i) by
.= yn . j by ;
hence ((bind (B,i,j)) # y19) . n = y2 . n by ; :: thesis: verum
end;
then for n being Nat st n in Seg (len ()) holds
One . n = Two . n by A61;
hence (bind (B,i,j)) # y19 = () . j by ; :: thesis: verum
end;
then (Den (o,(OAF . j))) . ((bind (B,i,j)) # y19) = ((OAF ?. o) . j) . (() . j) by PRALG_2:7
.= x1 . j by ;
hence ((bind (B,i,j)) . ) . (x1 . i) = x1 . j by ; :: thesis: verum
end;
suppose A68: the_arity_of o = {} ; :: thesis: ((bind (B,i,j)) . ) . (x1 . i) = x1 . j
reconsider 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 ((),{},(commute (OAF ?. o)),(Commute (Frege (OAF ?. o)))) by PRALG_2:def 13
.= commute (OAF ?. o) by ;
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; :: thesis: x1 . d = (Den (o,(OAF . d))) . {}
reconsider g = (OAF ?. o) . d as Function ;
A74: x1 = (commute (OAF ?. o)) . y by ;
g = Den (o,(OAF . d)) by PRALG_2:7;
then dom g = Args (o,(OAF . d)) by FUNCT_2:def 1
.= by ;
then A75: y in dom g by ;
then A76: [d,y] in dom (uncurry (OAF ?. o)) by ;
co . d = co9 . d by FUNCT_6:def 10
.= (uncurry (OAF ?. o)) . (d,y) by
.= g . y by ;
then x1 . d = (Den (o,(OAF . d))) . y by
.= (Den (o,(OAF . d))) . {} by ;
hence x1 . d = (Den (o,(OAF . d))) . {} ; :: thesis: verum
end;
then A77: x1 . i = (Den (o,(OAF . i))) . {} ;
Args (o,(OAF . i)) = by ;
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 ;
bind (B,i,j) is_homomorphism OAF . i,OAF . j by ;
then A79: ((bind (B,i,j)) . ) . (x1 . i) = (Den (o,(OAF . j))) . ((bind (B,i,j)) # E) by ;
x1 . j = (Den (o,(OAF . j))) . {} by A73;
hence ((bind (B,i,j)) . ) . (x1 . i) = x1 . j by ; :: thesis: verum
end;
end;
end;
then x in { f where f is Element of product (Carrier (OAF,)) : for i, j being Element of P st i >= j holds
((bind (B,i,j)) . ) . (f . i) = f . j
}
by A10;
hence x in C . by A1; :: thesis: verum
end;
then x in C . ;
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 ; :: thesis: verum
end;
hence C is_closed_on o by MSUALG_2:def 5; :: thesis: 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 ;
now :: thesis: for s being 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 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 )

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 ) :: thesis: verum
proof
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 . j

then 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 ;
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 ; :: 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 A83;
hence f in the Sorts of (L | C) . s by ; :: 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