set f = (Den (o,U0)) | (((A #) * the Arity of S) . o);
set B = the Sorts of U0;
A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

per cases ( (A * the ResultSort of S) . o = {} or (A * the ResultSort of S) . o <> {} ) ;

suppose A3: (A * the ResultSort of S) . o = {} ; :: thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1;
then A4: (Den (o,U0)) | (((A #) * the Arity of S) . o) = {} by A3;

now :: thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

per cases ( ((A #) * the Arity of S) . o = {} or ((A #) * the Arity of S) . o <> {} ) ;

suppose ((A #) * the Arity of S) . o = {} ; :: thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A4, RELSET_1:12; :: thesis: verum

end;

suppose ((A #) * the Arity of S) . o <> {} ; :: thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

thus (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A3, A4, FUNCT_2:def 1, RELSET_1:12; :: thesis: verum

end;

end;

end;

hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) ; :: thesis: verum

end;

suppose A5: (A * the ResultSort of S) . o <> {} ; :: thesis: (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

reconsider B0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
A6: A c= B0 by PBOOLE:def 18;
A7: rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1;
A c= the Sorts of U0 by PBOOLE:def 18;
then A . ( the ResultSort of S . o) c= the Sorts of U0 . ( the ResultSort of S . o) ;
then the Sorts of U0 . ( the ResultSort of S . o) <> {} by A2, A5, FUNCT_1:13;
then ( the Sorts of U0 * the ResultSort of S) . o <> {} by A2, FUNCT_1:13;
then Result (o,U0) <> {} by MSUALG_1:def 5;
then dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def 1
.= (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def 4 ;
then dom ((Den (o,U0)) | (((A #) * the Arity of S) . o)) = ((( the Sorts of U0 #) * the Arity of S) . o) /\ (((A #) * the Arity of S) . o) by RELAT_1:61
.= ((A #) * the Arity of S) . o by A6, Th2, XBOOLE_1:28 ;
hence (Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) by A7, FUNCT_2:2; :: thesis: verum

end;

end;