let I be non empty set ; :: thesis: for G being Group
for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds
1_ (product F) = I --> (1_ G)
let G be Group; :: thesis: for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds
1_ (product F) = I --> (1_ G)
let F be Group-Family of I; :: thesis: ( ( for i being Element of I holds F . i is Subgroup of G ) implies 1_ (product F) = I --> (1_ G) )
assume A1: for i being Element of I holds F . i is Subgroup of G ; :: thesis: 1_ (product F) = I --> (1_ G)
A2: dom (1_ (product F)) = I by Th3;
A3: dom (I --> (1_ G)) = I by FUNCOP_1:13;
for j being object st j in I holds
(1_ (product F)) . j = (I --> (1_ G)) . j

proof

let j be object ; :: thesis: ( j in I implies (1_ (product F)) . j = (I --> (1_ G)) . j )
assume A4: j in I ; :: thesis: (1_ (product F)) . j = (I --> (1_ G)) . j
then reconsider Z = F . j as Group by Th1;
A5: (1_ (product F)) . j = 1_ Z by A4, GROUP_7:6;
A6: (I --> (1_ G)) . j = 1_ G by A4, FUNCOP_1:7;
reconsider j = j as Element of I by A4;
F . j is Subgroup of G by A1;
hence (1_ (product F)) . j = (I --> (1_ G)) . j by A5, A6, GROUP_2:44; :: thesis: verum

end;

hence 1_ (product F) = I --> (1_ G) by A2, A3, FUNCT_1:2; :: thesis: verum