reconsider L = product OAF as non-empty MSAlgebra over S ;

deffunc H_{1}( 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 = H_{1}(s)
from PBOOLE:sch 5();

for i being object st i in the carrier of S holds

C . i c= (SORTS OAF) . i

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

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;

_{1} 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 b_{1} . s iff for i, j being Element of P st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j ) ; :: thesis: verum

deffunc H

((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 = H

for i being object st i in the carrier of S holds

C . i c= (SORTS OAF) . i

proof

then
C c= SORTS OAF
by PBOOLE:def 2;
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 S_{1}[ 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)) : S_{1}[f] } c= product (Carrier (OAF,s))
from FRAENKEL:sch 10();

(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;assume i in the carrier of S ; :: thesis: C . i c= (SORTS OAF) . i

then reconsider s = i as SortSymbol of S ;

defpred S

((bind (B,i,j)) . s) . ($1 . i) = $1 . j;

A2: { f where f is Element of product (Carrier (OAF,s)) : S

(SORTS OAF) . s = product (Carrier (OAF,s)) by PRALG_2:def 10;

hence C . i c= (SORTS OAF) . i by A1, A2; :: thesis: verum

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

then A81:
C is opers_closed
by MSUALG_2:def 6;
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

end;rng ((Den (o,(product OAF))) | (((C #) * the Arity of S) . o)) c= (C * the ResultSort of S) . o

proof

hence
C is_closed_on o
by MSUALG_2:def 5; :: thesis: verum
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 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;

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; :: thesis: verum

end;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 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 :: thesis: for s being SortSymbol of S holds x in C . (the_result_sort_of o)

then
x in C . (the_result_sort_of o)
;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

((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; :: thesis: verum

end;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

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
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)) . (the_result_sort_of o)) . (x1 . i) = x1 . j )

assume A13: i >= j ; :: thesis: ((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 A17: dom y = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;

rng y c= Funcs ( the carrier of P,|.OAF.|)

end;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)) . (the_result_sort_of o)) . (x1 . i) = x1 . j )

assume A13: i >= j ; :: thesis: ((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

proof

then A16:
dom y = dom (the_arity_of o)
by A14, RELAT_1:27;
let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (the_arity_of o) or i in dom MS )

assume i in rng (the_arity_of o) ; :: thesis: i in dom MS

then i in the carrier of S ;

hence i in dom MS by PARTFUN1:def 2; :: thesis: verum

end;assume i in rng (the_arity_of o) ; :: thesis: i in dom MS

then i in the carrier of S ;

hence i in dom MS by PARTFUN1:def 2; :: thesis: verum

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

then A28:
y in Funcs ((Seg (len (the_arity_of o))),(Funcs ( the carrier of P,|.OAF.|)))
by A17, FUNCT_2:def 2;
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 * (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.|

end;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 * (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

hence
z in Funcs ( the carrier of P,|.OAF.|)
by A22, FUNCT_2:def 2; :: thesis: verum
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 A22, A23;

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 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; :: thesis: verum

end;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 A22, A23;

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 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; :: thesis: verum

per cases
( the_arity_of o <> {} or the_arity_of o = {} )
;

end;

suppose A29:
the_arity_of o <> {}
; :: thesis: ((bind (B,i,j)) . (the_result_sort_of o)) . (x1 . i) = x1 . j

A30:
for t being object st t in dom (doms (OAF ?. o)) holds

Co . t in (doms (OAF ?. o)) . t

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))

A57: bind (B,i,j) is_homomorphism OAF . i,OAF . j by A13, Th2;

(bind (B,i,j)) # y19 = (commute y) . j

.= 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; :: thesis: verum

end;Co . t in (doms (OAF ?. o)) . t

proof

A42:
Co in product (doms (OAF ?. o))
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 (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))

hence Co . t in (doms (OAF ?. o)) . t by A32, PRALG_2:3; :: thesis: verum

end;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 (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

(doms (OAF ?. o)) . t = Args (o,(OAF . t))
by PRALG_2:11;
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 object 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

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; :: thesis: verum

end;.= 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 object 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

Co . t in rng Co
by A31, FUNCT_1:def 3;
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 object ; :: 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 )

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)) ; :: thesis: 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 over 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; :: thesis: verum

end;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 object ; :: 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 )

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)) ; :: thesis: 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 over 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; :: thesis: verum

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; :: thesis: verum

hence Co . t in (doms (OAF ?. o)) . t by A32, PRALG_2:3; :: thesis: verum

proof

A43:
OPE = IFEQ ((the_arity_of o),{},(commute (OAF ?. o)),(Commute (Frege (OAF ?. o))))
by PRALG_2:def 13;
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 ex Co9 being Function st

( Co9 = Co & dom Co9 = the carrier of P & rng Co9 c= Funcs ((Seg (len (the_arity_of o))),|.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 A30, CARD_3:9; :: thesis: verum

end;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 ex Co9 being Function st

( Co9 = Co & dom Co9 = the carrier of P & rng Co9 c= Funcs ((Seg (len (the_arity_of o))),|.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 A30, CARD_3:9; :: thesis: verum

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

then reconsider y19 = y1 as Element of Args (o,(OAF . i)) by PRALG_2:3;
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 object 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

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; :: thesis: verum

end;.= Seg (len (the_arity_of o)) by FINSEQ_1:def 3 ;

A50: for w being object 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

Co . i in rng Co
by A48, FUNCT_1:def 3;
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 object ; :: 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 )

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)) ; :: thesis: 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 over 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; :: thesis: verum

end;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 object ; :: 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 )

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)) ; :: thesis: 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 over 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; :: thesis: verum

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; :: thesis: verum

A57: bind (B,i,j) is_homomorphism OAF . i,OAF . j by A13, Th2;

(bind (B,i,j)) # y19 = (commute y) . j

proof

then (Den (o,(OAF . j))) . ((bind (B,i,j)) # y19) =
((OAF ?. o) . j) . ((commute y) . j)
by PRALG_2:7
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;

One . n = Two . n by A61;

hence (bind (B,i,j)) # y19 = (commute y) . j by A61, A58, FINSEQ_1:13; :: thesis: verum

end;.= 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 :: thesis: for n being Nat st n in dom y2 holds

((bind (B,i,j)) # y19) . n = y2 . n

then
for n being Nat st n in Seg (len (the_arity_of o)) 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 = (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 ; :: thesis: ((bind (B,i,j)) # y19) . n = y2 . n

then 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; :: thesis: verum

end;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 ; :: thesis: ((bind (B,i,j)) # y19) . n = y2 . n

then 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; :: thesis: verum

One . n = Two . n by A61;

hence (bind (B,i,j)) # y19 = (commute y) . j by A61, A58, FINSEQ_1:13; :: thesis: verum

.= 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; :: thesis: verum

suppose A68:
the_arity_of o = {}
; :: thesis: ((bind (B,i,j)) . (the_result_sort_of o)) . (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 ((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))) . {}

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; :: thesis: verum

end;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

then A77:
x1 . i = (Den (o,(OAF . i))) . {}
;
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 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))) . {} ; :: thesis: verum

end;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 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))) . {} ; :: thesis: verum

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; :: thesis: verum

((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; :: thesis: verum

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; :: thesis: verum

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 :: 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 )

hence
ex bfor 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

end;( 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

((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 A1, A82; :: thesis: verum

end;

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
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 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 ; :: thesis: verum

end;((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 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 ; :: thesis: verum

((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 A1, A82; :: thesis: verum

for s being SortSymbol of S

for f being Element of (SORTS OAF) . s holds

( f in the Sorts of b

((bind (B,i,j)) . s) . (f . i) = f . j ) ; :: thesis: verum