let i be Element of P; :: according to MSALIMIT:def 4 :: thesis: (Normalized B) . (i,i) = id the Sorts of (OAF . i)

i >= i by ORDERS_2:1;

then (Normalized B) . (i,i) = IFEQ (i,i,(id the Sorts of (OAF . i)),((bind (B,i,i)) ** (id the Sorts of (OAF . i)))) by Def5;

hence (Normalized B) . (i,i) = id the Sorts of (OAF . i) by FUNCOP_1:def 8; :: thesis: verum

i >= i by ORDERS_2:1;

then (Normalized B) . (i,i) = IFEQ (i,i,(id the Sorts of (OAF . i)),((bind (B,i,i)) ** (id the Sorts of (OAF . i)))) by Def5;

hence (Normalized B) . (i,i) = id the Sorts of (OAF . i) by FUNCOP_1:def 8; :: thesis: verum