let P be non empty Poset; :: thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
() . (j,i) = NB . (j,i)

let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
() . (j,i) = NB . (j,i)

let OAF be OrderedAlgFam of P,S; :: thesis: for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
() . (j,i) = NB . (j,i)

let NB be normalized Binding of OAF; :: thesis: for i, j being Element of P st i >= j holds
() . (j,i) = NB . (j,i)

let i, j be Element of P; :: thesis: ( i >= j implies () . (j,i) = NB . (j,i) )
assume A1: i >= j ; :: thesis: () . (j,i) = NB . (j,i)
per cases ( i <> j or i = j ) ;
suppose i <> j ; :: thesis: () . (j,i) = NB . (j,i)
hence (Normalized NB) . (j,i) = NB . (j,i) by ; :: thesis: verum
end;
suppose A2: i = j ; :: thesis: () . (j,i) = NB . (j,i)
(Normalized NB) . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (NB,i,j)) ** (id the Sorts of (OAF . i)))) by ;
then (Normalized NB) . (j,i) = id the Sorts of (OAF . i) by ;
hence (Normalized NB) . (j,i) = NB . (j,i) by ; :: thesis: verum
end;
end;