set G = the Group;
deffunc H1( 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 = H1(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