let G be Group; :: thesis: for I being empty set
for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff G is trivial )
let I be empty set ; :: thesis: for F being Subgroup-Family of I,G holds
( G is_internal_product_of F iff G is trivial )
let F be Subgroup-Family of I,G; :: thesis: ( G is_internal_product_of F iff G is trivial )
thus ( G is_internal_product_of F implies G is trivial ) by ThJoinEmptyGr; :: thesis: ( G is trivial implies G is_internal_product_of F )
assume G is trivial ; :: thesis: G is_internal_product_of F
then multMagma(# the carrier of G, the multF of G #) = (1). G by GROUP_22:6;
hence G is_internal_product_of F by ThJoinEmptyGr; :: thesis: verum