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 set st s in the carrier of S holds
the Sorts of (InvLim B) . s = the Sorts of (product OAF) . s

proof

let a be set ; :: 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 set ; :: 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 10;
then the Sorts of (InvLim B) c= the Sorts of (product OAF) by PBOOLE:def 23;
then A2: the Sorts of (InvLim B) . s c= the Sorts of (product OAF) . s by PBOOLE:def 5;
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 set ; :: 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:20;
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 4, PRALG_2:def 17;
then A4: f . i in (Carrier OAF,s) . i by CARD_3:18;
bind B,i,i = B . i,i by Def3, ORDERS_2:24
.= 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 of S st
( U0 = OAF . i & (Carrier OAF,s) . i = the Sorts of U0 . s ) by PRALG_2:def 16;
hence ((bind B,i,j) . s) . (f . i) = f . j by A3, A5, A4, FUNCT_1:35; :: 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:6;
hence InvLim B = product OAF by A1, MSUALG_2:10, PBOOLE:3; :: thesis: verum