set G = the non empty multMagma ;
deffunc H₁( 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 = H₁(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
let i be Element of I; :: thesis: f . i is multMagma-Family of J . i
(J . i) --> the non empty multMagma = f . i by A1;
hence f . i is multMagma-Family of J . i ; :: thesis: verum