const o,(product A) is Function

proof

per cases ( the_arity_of o = {} or the_arity_of o <> {} ) ;

suppose the_arity_of o = {} ; :: thesis: const o,(product A) is Function

then const o,(product A) in Funcs I,(union { (Result o,(A . i9)) where i9 is Element of I : verum } ) by Th9;
then ex g being Function st
( g = const o,(product A) & dom g = I & rng g c= union { (Result o,(A . i9)) where i9 is Element of I : verum } ) by FUNCT_2:def 2;
hence const o,(product A) is Function ; :: thesis: verum

end;

suppose A1: the_arity_of o <> {} ; :: thesis: const o,(product A) is Function

dom (the Sorts of (product A) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:10;
then A2: dom (the Sorts of (product A) * (the_arity_of o)) <> dom {} by A1;
dom (Den o,(product A)) = Args o,(product A) by FUNCT_2:def 1
.= product (the Sorts of (product A) * (the_arity_of o)) by PRALG_2:10 ;
then not {} in dom (Den o,(product A)) by A2, CARD_3:18;
hence const o,(product A) is Function by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence ( const o,(product A) is Relation-like & const o,(product A) is Function-like ) ; :: thesis: verum