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