let I be set ; :: thesis: for F being Function st I = dom F & ( for i being object st i in I holds
F . i is Group ) holds
F is Group-Family of I
let F be Function; :: thesis: ( I = dom F & ( for i being object st i in I holds
F . i is Group ) implies F is Group-Family of I )
assume A1: I = dom F ; :: thesis: ( ex i being object st
( i in I & F . i is not Group ) or F is Group-Family of I )
assume A2: for i being object st i in I holds
F . i is Group ; :: thesis: F is Group-Family of I
reconsider F = F as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for y being set st y in rng F holds
y is non empty multMagma

let y be set ; :: thesis: ( y in rng F implies y is non empty multMagma )
assume y in rng F ; :: thesis: y is non empty multMagma
then consider i being object such that
A3: ( i in dom F & y = F . i ) by FUNCT_1:def 3;
thus y is non empty multMagma by A2, A3; :: thesis: verum

end;

then reconsider F = F as multMagma-Family of I by GROUP_7:def 1;
A4: for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i

proof

let i be set ; :: thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = F . i )
assume i in I ; :: thesis: ex Fi being non empty Group-like multMagma st Fi = F . i
then reconsider Fi = F . i as non empty Group-like multMagma by A2;
take Fi ; :: thesis: Fi = F . i
thus Fi = F . i ; :: thesis: verum

end;

for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i

proof

let i be set ; :: thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = F . i )
assume i in I ; :: thesis: ex Fi being non empty associative multMagma st Fi = F . i
then reconsider Fi = F . i as non empty associative multMagma by A2;
take Fi ; :: thesis: Fi = F . i
thus Fi = F . i ; :: thesis: verum

end;

hence F is Group-Family of I by A4, GROUP_7:def 3, GROUP_7:def 4; :: thesis: verum