let G be Group; :: thesis: for I being empty set
for F being Subgroup-Family of I,G holds gr (Union (Carrier F)) = (1). G
let I be empty set ; :: thesis: for F being Subgroup-Family of I,G holds gr (Union (Carrier F)) = (1). G
let F be Subgroup-Family of I,G; :: thesis: gr (Union (Carrier F)) = (1). G
Carrier F = {} --> (bool the carrier of G) ;
then Union (Carrier F) = {} by FUNCT_6:26;
then Union (Carrier F) = {} the carrier of G by SUBSET_1:def 2;
hence gr (Union (Carrier F)) = (1). G by GROUP_4:30; :: thesis: verum