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;