reconsider H = prod_bundle F as Group-Family of I ;
dprod F = product H ;
hence ( dprod F is Group-like & dprod F is associative ) ; :: thesis: verum