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

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 A5, 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 A4, A5, 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 (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)

then A6: A . (the ResultSort of S . o) <> {} by A2, FUNCT_1:23;
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 A6;
then (the Sorts of U0 * the ResultSort of S) . o <> {} by A2, FUNCT_1:23;
then A8: Result o,U0 <> {} by MSUALG_1:def 10;
reconsider B0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 23;
A9: A c= B0 by PBOOLE:def 23;
dom (Den o,U0) = Args o,U0 by A8, FUNCT_2:def 1
.= ((the Sorts of U0 # ) * the Arity of S) . o by MSUALG_1:def 9 ;
then A10: 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 A9, Th3, XBOOLE_1:28 ;
rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (A * the ResultSort of S) . o by A1, Def6;
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 A10, FUNCT_2:4; :: thesis: verum

end;

end;