let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being multMagma-Family of J
for x being Element of (product F) holds x * a in product (F * a)
let a be Function of I,J; :: thesis: for F being multMagma-Family of J
for x being Element of (product F) holds x * a in product (F * a)
let F be multMagma-Family of J; :: thesis: for x being Element of (product F) holds x * a in product (F * a)
let x be Element of (product F); :: thesis: x * a in product (F * a)
dom x = J by GROUP_19:3;
then rng a c= dom x ;
then dom (x * a) = dom a by RELAT_1:27;
then dom (x * a) = I by PARTFUN1:def 2;
then reconsider y = x * a as ManySortedSet of I by PARTFUN1:def 2;
reconsider z = Carrier (F * a) as ManySortedSet of I ;
A1: dom y = I by PARTFUN1:def 2;
A2: dom z = I by PARTFUN1:def 2;
A3: dom a = I by PARTFUN1:def 2;
for i being object st i in I holds
y . i in z . i

proof

let i be object ; :: thesis: ( i in I implies y . i in z . i )
assume i in I ; :: thesis: y . i in z . i
then reconsider i = i as Element of I ;
reconsider j = a . i as Element of J ;
A4: z . i = [#] ((F * a) . i) by PENCIL_3:7
.= [#] (F . j) by A3, FUNCT_1:13 ;
x in product F ;
then x . j in F . j by GROUP_19:5;
hence y . i in z . i by A3, A4, FUNCT_1:13; :: thesis: verum

end;

then y in product z by A1, A2, CARD_3:def 5;
hence x * a in product (F * a) by GROUP_7:def 2; :: thesis: verum