let I be set ; :: thesis: for G being Group
for F being Group-Family of I
for a being object st a in sum F & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
a is finite-support Function of I,G
let G be Group; :: thesis: for F being Group-Family of I
for a being object st a in sum F & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
a is finite-support Function of I,G
let F be Group-Family of I; :: thesis: for a being object st a in sum F & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
a is finite-support Function of I,G
let a be object ; :: thesis: ( a in sum F & ( for i being object st i in I holds
F . i is Subgroup of G ) implies a is finite-support Function of I,G )
assume that
A1: a in sum F and
A2: for i being object st i in I holds
F . i is Subgroup of G ; :: thesis: a is finite-support Function of I,G
a in product F by A1, GROUP_2:40;
then reconsider b = a as Element of (product F) ;
A8: dom b = I by Th3;
for z being object st z in rng b holds
z in [#] G

proof

let z be object ; :: thesis: ( z in rng b implies z in [#] G )
assume z in rng b ; :: thesis: z in [#] G
then consider i being object such that
A9: ( i in dom b & z = b . i ) by FUNCT_1:def 3;
i in I by A9, Th3;
then reconsider Z = F . i as Subgroup of G by A2;
reconsider I = I as non empty set by A9, Th3;
reconsider i = i as Element of I by A9, Th3;
reconsider F = F as multMagma-Family of I ;
b . i in F . i by A1, Th5, GROUP_2:40;
then b . i in Z ;
then b . i in G by GROUP_2:40;
hence z in [#] G by A9; :: thesis: verum

end;

then rng b c= [#] G ;
then reconsider b = b as Function of I,G by A8, FUNCT_2:2;
support (b,F) = support b by A2, Th9;
hence a is finite-support Function of I,G by A1, Def3; :: thesis: verum