now :: thesis: for x being Element of (sum F) holds x is Function
let x be Element of (sum F); :: thesis: x is Function
x is Element of (product F) by GROUP_2:42;
hence x is Function ; :: thesis: verum
end;
hence ( not sum F is empty & sum F is constituted-Functions ) ; :: thesis: verum