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