then const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by Th8;
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

dom ( the Sorts of (product A) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3;
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:3 ;
then not {} in dom (Den (o,(product A))) by A2, CARD_3:9;
hence const (o,(product A)) is Function by FUNCT_1:def 2; :: thesis: verum