set G = the non empty multMagma ;
deffunc H1( object ) -> Element of bool [:(J . $1),{ the non empty multMagma }:] = (J . $1) --> the non empty multMagma ;
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;
take f ; :: thesis: for i being Element of I holds f . i is multMagma-Family of J . i
for i being Element of I holds f . i is multMagma-Family of J . i
proof
let i be Element of I; :: thesis: f . i is multMagma-Family of J . i
set fi = (J . i) --> the non empty multMagma ;
A2: (J . i) --> the non empty multMagma = f . i by A1;
for a being set st a in rng ((J . i) --> the non empty multMagma ) holds
a is non empty multMagma by TARSKI:def 1;
hence f . i is multMagma-Family of J . i by A2, GROUP_7:def 1; :: thesis: verum
end;
hence for i being Element of I holds f . i is multMagma-Family of J . i ; :: thesis: verum