j >= j by ORDERS_2:24;
then ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . j) st
( f1 = B . j,i & f2 = B . j,j & B . j,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;
hence B . j,i is ManySortedFunction of (OAF . i),(OAF . j) ; :: thesis: verum