let P be non empty Poset; 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 ; 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; 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; 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; ( i >= j implies (Normalized NB) . (j,i) = NB . (j,i) )
assume A1:
i >= j
; (Normalized NB) . (j,i) = NB . (j,i)
per cases
( i <> j or i = j )
;
suppose A2:
i = j
;
(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;
verum end; end;