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