( [f,g] `1 = f & [f,g] `2 = g ) ;
hence [f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B by Def5, Def6; :: thesis: verum