reconsider G = F as ManySortedFunction of A,B * [:f,f:] by Def4;
~ G is ManySortedFunction of ~ A,(~ B) * [:f,f:] by ALTCAT_2:3;
hence ~ F is MSUnTrans of [:f,f:], ~ A, ~ B by Def4; :: thesis: verum