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 that

A1: i >= j and

A2: i <> j ; :: thesis: B . (j,i) = (Normalized B) . (j,i)

( (Normalized B) . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) & 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, A2, Def5, FUNCOP_1:def 8;

then (Normalized B) . (j,i) = bind (B,i,j) by MSUALG_3:3;

hence B . (j,i) = (Normalized B) . (j,i) by A1, Def3; :: thesis: verum

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 that

A1: i >= j and

A2: i <> j ; :: thesis: B . (j,i) = (Normalized B) . (j,i)

( (Normalized B) . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) & 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, A2, Def5, FUNCOP_1:def 8;

then (Normalized B) . (j,i) = bind (B,i,j) by MSUALG_3:3;

hence B . (j,i) = (Normalized B) . (j,i) by A1, Def3; :: thesis: verum