let P be non empty Poset; :: thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . j,i = (Normalized B) . j,i
let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of P,S
for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . j,i = (Normalized B) . j,i
let OAF be OrderedAlgFam of P,S; :: thesis: for B being Binding of OAF
for i, j being Element of P st i >= j & i <> j holds
B . j,i = (Normalized B) . j,i
let B be Binding of OAF; :: thesis: for i, j being Element of P st i >= j & i <> j holds
B . j,i = (Normalized B) . j,i
let i, j be Element of P; :: thesis: ( i >= j & i <> j implies B . j,i = (Normalized B) . j,i )
assume A1: ( i >= j & i <> j ) ; :: thesis: B . j,i = (Normalized B) . j,i
then A2: (Normalized B) . j,i = IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i))) by Def5;
IFEQ j,i,(id the Sorts of (OAF . i)),((bind B,i,j) ** (id the Sorts of (OAF . i))) = (bind B,i,j) ** (id the Sorts of (OAF . i)) by A1, FUNCOP_1:def 8;
then (Normalized B) . j,i = bind B,i,j by A2, MSUALG_3:3;
hence B . j,i = (Normalized B) . j,i by A1, Def3; :: thesis: verum