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, Def6;
then A4: (Den o,U0) | (((A # ) * the Arity of S) . o) = {} by A3;

now

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:25; :: 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)

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 A3, A4, FUNCT_2:def 1, RELSET_1:25; :: 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 23;
A6: A c= B0 by PBOOLE:def 23;
A7: rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def6;
A c= the Sorts of U0 by PBOOLE:def 23;
then A . (the ResultSort of S . o) c= the Sorts of U0 . (the ResultSort of S . o) by PBOOLE:def 5;
then the Sorts of U0 . (the ResultSort of S . o) <> {} by A2, A5, FUNCT_1:23;
then (the Sorts of U0 * the ResultSort of S) . o <> {} by A2, FUNCT_1:23;
then Result o,U0 <> {} by MSUALG_1:def 10;
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 9 ;
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:90
.= ((A # ) * the Arity of S) . o by A6, Th3, 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:4; :: thesis: verum

end;

end;