let I be non empty set ; :: thesis: for F being Group-Family of I
for G being Group
for x being finite-support Function of I,G st support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
x = 1_ (product F)
let F be Group-Family of I; :: thesis: for G being Group
for x being finite-support Function of I,G st support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
x = 1_ (product F)
let G be Group; :: thesis: for x being finite-support Function of I,G st support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
x = 1_ (product F)
let x be finite-support Function of I,G; :: thesis: ( support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) implies x = 1_ (product F) )
assume that
A1: support x = {} and
A2: for i being object st i in I holds
F . i is Subgroup of G ; :: thesis: x = 1_ (product F)
for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & x . i = 1_ G )

proof

let i be set ; :: thesis: ( i in I implies ex G being non empty Group-like multMagma st
( G = F . i & x . i = 1_ G ) )
assume A3: i in I ; :: thesis: ex G being non empty Group-like multMagma st
( G = F . i & x . i = 1_ G )
then A4: x . i = 1_ G by A1, Def2;
reconsider Fi = F . i as Subgroup of G by A2, A3;
take Fi ; :: thesis: ( Fi = F . i & x . i = 1_ Fi )
thus ( Fi = F . i & x . i = 1_ Fi ) by A4, GROUP_2:44; :: thesis: verum

end;

hence x = 1_ (product F) by GROUP_7:5; :: thesis: verum