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