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

proof

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

proof

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;

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

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;

hence e in the Sorts of (InvLim B) . a by Def6; :: thesis: verum

end;

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