let A, B, O be Ordinal; :: thesis: ( O c= A & A c= B implies (unique_No_op A) . O = (unique_No_op B) . O )
assume A1: ( O c= A & A c= B ) ; :: thesis: (unique_No_op A) . O = (unique_No_op B) . O
O in succ A by A1, ORDINAL1:6, ORDINAL1:12;
then ((unique_No_op B) | (succ A)) . O = (unique_No_op B) . O by FUNCT_1:49;
hence (unique_No_op A) . O = (unique_No_op B) . O by A1, Th37; :: thesis: verum