o in the carrier' of S ;
then o in dom ( the Sorts of A * the ResultSort of S) by PARTFUN1:def 2;
then ( the Sorts of A * the ResultSort of S) . o in rng ( the Sorts of A * the ResultSort of S) by FUNCT_1:def 3;
hence ( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A by FUNCT_1:14; :: thesis: verum