let DP be non empty discrete Poset; :: thesis: for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

let OAF be OrderedAlgFam of DP,S; :: thesis: for B being normalized Binding of OAF holds InvLim B = product OAF

let B be normalized Binding of OAF; :: thesis: InvLim B = product OAF

A1: for s being object st s in the carrier of S holds

the Sorts of (InvLim B) . s = the Sorts of (product OAF) . s

hence InvLim B = product OAF by A1, MSUALG_2:9, PBOOLE:3; :: thesis: verum

for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of DP,S

for B being normalized Binding of OAF holds InvLim B = product OAF

let OAF be OrderedAlgFam of DP,S; :: thesis: for B being normalized Binding of OAF holds InvLim B = product OAF

let B be normalized Binding of OAF; :: thesis: InvLim B = product OAF

A1: for s being object st s in the carrier of S holds

the Sorts of (InvLim B) . s = the Sorts of (product OAF) . s

proof

product OAF is MSSubAlgebra of product OAF
by MSUALG_2:5;
let a be object ; :: thesis: ( a in the carrier of S implies the Sorts of (InvLim B) . a = the Sorts of (product OAF) . a )

assume a in the carrier of S ; :: thesis: the Sorts of (InvLim B) . a = the Sorts of (product OAF) . a

then reconsider s = a as SortSymbol of S ;

thus the Sorts of (InvLim B) . a c= the Sorts of (product OAF) . a :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (product OAF) . a c= the Sorts of (InvLim B) . a

assume e in the Sorts of (product OAF) . a ; :: thesis: e in the Sorts of (InvLim B) . a

then reconsider f = e as Element of (SORTS OAF) . s by PRALG_2:12;

for i, j being Element of DP st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j

end;assume a in the carrier of S ; :: thesis: the Sorts of (InvLim B) . a = the Sorts of (product OAF) . a

then reconsider s = a as SortSymbol of S ;

thus the Sorts of (InvLim B) . a c= the Sorts of (product OAF) . a :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (product OAF) . a c= the Sorts of (InvLim B) . a

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Sorts of (product OAF) . a or e in the Sorts of (InvLim B) . a )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the Sorts of (InvLim B) . a or e in the Sorts of (product OAF) . a )

the Sorts of (InvLim B) is MSSubset of (product OAF) by MSUALG_2:def 9;

then the Sorts of (InvLim B) c= the Sorts of (product OAF) by PBOOLE:def 18;

then A2: the Sorts of (InvLim B) . s c= the Sorts of (product OAF) . s by PBOOLE:def 2;

assume e in the Sorts of (InvLim B) . a ; :: thesis: e in the Sorts of (product OAF) . a

hence e in the Sorts of (product OAF) . a by A2; :: thesis: verum

end;the Sorts of (InvLim B) is MSSubset of (product OAF) by MSUALG_2:def 9;

then the Sorts of (InvLim B) c= the Sorts of (product OAF) by PBOOLE:def 18;

then A2: the Sorts of (InvLim B) . s c= the Sorts of (product OAF) . s by PBOOLE:def 2;

assume e in the Sorts of (InvLim B) . a ; :: thesis: e in the Sorts of (product OAF) . a

hence e in the Sorts of (product OAF) . a by A2; :: thesis: verum

assume e in the Sorts of (product OAF) . a ; :: thesis: e in the Sorts of (InvLim B) . a

then reconsider f = e as Element of (SORTS OAF) . s by PRALG_2:12;

for i, j being Element of DP st i >= j holds

((bind (B,i,j)) . s) . (f . i) = f . j

proof

hence
e in the Sorts of (InvLim B) . a
by Def6; :: thesis: verum
let i, j be Element of DP; :: thesis: ( i >= j implies ((bind (B,i,j)) . s) . (f . i) = f . j )

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

then A3: i = j by ORDERS_3:1;

f in (SORTS OAF) . s ;

then ( dom (Carrier (OAF,s)) = the carrier of DP & f in product (Carrier (OAF,s)) ) by PARTFUN1:def 2, PRALG_2:def 10;

then A4: f . i in (Carrier (OAF,s)) . i by CARD_3:9;

bind (B,i,i) = B . (i,i) by Def3, ORDERS_2:1

.= id the Sorts of (OAF . i) by Def4 ;

then A5: (bind (B,i,i)) . s = id ( the Sorts of (OAF . i) . s) by MSUALG_3:def 1;

ex U0 being MSAlgebra over S st

( U0 = OAF . i & (Carrier (OAF,s)) . i = the Sorts of U0 . s ) by PRALG_2:def 9;

hence ((bind (B,i,j)) . s) . (f . i) = f . j by A3, A5, A4, FUNCT_1:18; :: thesis: verum

end;assume i >= j ; :: thesis: ((bind (B,i,j)) . s) . (f . i) = f . j

then A3: i = j by ORDERS_3:1;

f in (SORTS OAF) . s ;

then ( dom (Carrier (OAF,s)) = the carrier of DP & f in product (Carrier (OAF,s)) ) by PARTFUN1:def 2, PRALG_2:def 10;

then A4: f . i in (Carrier (OAF,s)) . i by CARD_3:9;

bind (B,i,i) = B . (i,i) by Def3, ORDERS_2:1

.= id the Sorts of (OAF . i) by Def4 ;

then A5: (bind (B,i,i)) . s = id ( the Sorts of (OAF . i) . s) by MSUALG_3:def 1;

ex U0 being MSAlgebra over S st

( U0 = OAF . i & (Carrier (OAF,s)) . i = the Sorts of U0 . s ) by PRALG_2:def 9;

hence ((bind (B,i,j)) . s) . (f . i) = f . j by A3, A5, A4, FUNCT_1:18; :: thesis: verum

hence InvLim B = product OAF by A1, MSUALG_2:9, PBOOLE:3; :: thesis: verum