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)

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 )
;

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;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