consider U0 being MSAlgebra of S such that
A2: ( U0 = AF . i & (OPER AF) . i = the Charact of U0 ) by PRALG_2:def 18;
thus ( ((OPER AF) . i) . o is Function-like & ((OPER AF) . i) . o is Relation-like ) by A2; :: thesis: verum