ex U0 being MSAlgebra over S st
( U0 = AF . i & (OPER AF) . i = the Charact of U0 ) by PRALG_2:def 11;
hence ( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like ) ; :: thesis: verum