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