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
f . i = (J . i) --> the Group by A1;
hence f . i is Group-Family of J . i ; :: 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