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