let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I st I is trivial holds
F . i, product F are_isomorphic
let i be Element of I; :: thesis: for F being Group-Family of I st I is trivial holds
F . i, product F are_isomorphic
let F be Group-Family of I; :: thesis: ( I is trivial implies F . i, product F are_isomorphic )
assume I is trivial ; :: thesis: F . i, product F are_isomorphic
then reconsider I = I as 1 -element set ;
set h = proj (F,i);
proj (F,i) is onto by GROUP_23:33;
then A1: rng (proj (F,i)) = the carrier of (F . i) by FUNCT_2:def 3;
reconsider i = i as Element of I ;
proj (F,i) = proj ((Carrier F),i) by GROUP_23:36;
then proj (F,i) is bijective by A1, GROUP_6:60;
hence F . i, product F are_isomorphic by GROUP_6:def 11; :: thesis: verum