set G = the Group;
deffunc H₁( object ) -> Element of bool [:(J . $1),{ the Group}:] = (J . $1) --> the Group;
consider f being Function such that
A1: ( dom f = I & ( for i being set st i in I holds
f . i = H₁(i) ) ) from FUNCT_1:sch 5();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;
A2: for i being Element of I holds f . i is Group-Family of J . i

proof

let i be Element of I; :: thesis: f . i is Group-Family of J . i
set fi = (J . i) --> the Group;
A3: f . i = (J . i) --> the Group by A1;
A4: dom ((J . i) --> the Group) = J . i by FUNCOP_1:13;
for k being object st k in J . i holds
((J . i) --> the Group) . k is Group by FUNCOP_1:7;
hence f . i is Group-Family of J . i by A3, A4, GROUP_19:2; :: thesis: verum

end;

then for i being Element of I holds f . i is multMagma-Family of J . i ;
then reconsider f = f as multMagma-Family of I,J by Def4;
take f ; :: thesis: for i being Element of I holds f . i is Group-Family of J . i
thus for i being Element of I holds f . i is Group-Family of J . i by A2; :: thesis: verum