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
(Normalized NB) . 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
(Normalized NB) . 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
(Normalized NB) . j,i = NB . j,i
let NB be normalized Binding of OAF; :: thesis: for i, j being Element of P st i >= j holds
(Normalized NB) . j,i = NB . j,i
let i, j be Element of P; :: thesis: ( i >= j implies (Normalized NB) . j,i = NB . j,i )
assume A1: i >= j ; :: thesis: (Normalized NB) . j,i = NB . j,i

per cases ( i <> j or i = j ) ;

suppose i <> j ; :: thesis: (Normalized NB) . j,i = NB . j,i

hence (Normalized NB) . j,i = NB . j,i by A1, Th3; :: thesis: verum

end;

suppose A2: i = j ; :: thesis: (Normalized NB) . 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 A1, Def5;
then (Normalized NB) . j,i = id the Sorts of (OAF . i) by A2, FUNCOP_1:def 8;
hence (Normalized NB) . j,i = NB . j,i by A2, Def4; :: thesis: verum

end;

end;