j >= j by ORDERS_2:24;
then consider f1 being ManySortedFunction of (OAF . i),(OAF . j), f2 being ManySortedFunction of (OAF . j),(OAF . j) such that
A2: ( f1 = B . j,i & f2 = B . j,j & B . j,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;
thus B . j,i is ManySortedFunction of (OAF . i),(OAF . j) by A2; :: thesis: verum