j >= j by ORDERS_2:1;
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