let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being multMagma-Family of J
for y being Element of (product (F * a)) st a is bijective holds
y * (a ") in product F
let a be Function of I,J; :: thesis: for F being multMagma-Family of J
for y being Element of (product (F * a)) st a is bijective holds
y * (a ") in product F
let F be multMagma-Family of J; :: thesis: for y being Element of (product (F * a)) st a is bijective holds
y * (a ") in product F
let y be Element of (product (F * a)); :: thesis: ( a is bijective implies y * (a ") in product F )
assume A1: a is bijective ; :: thesis: y * (a ") in product F
then A2: ( dom a = I & rng a = J ) by GROUP_6:61;
then A3: ( dom (a ") = J & rng (a ") = I ) by A1, FUNCT_1:33;
set x = y * (a ");
dom y = I by GROUP_19:3;
then A4: dom (y * (a ")) = J by A3, RELAT_1:27;
A5: dom (Carrier F) = J by PARTFUN1:def 2;
for j being object st j in J holds
(y * (a ")) . j in (Carrier F) . j
proof
let j be object ; :: thesis: ( j in J implies (y * (a ")) . j in (Carrier F) . j )
assume j in J ; :: thesis: (y * (a ")) . j in (Carrier F) . j
then reconsider j = j as Element of J ;
consider i being object such that
A6: ( i in I & j = a . i ) by A2, FUNCT_1:def 3;
reconsider i = i as Element of I by A6;
i = (a ") . j by A1, A2, A6, FUNCT_1:32;
then A7: (y * (a ")) . j = y . i by A3, FUNCT_1:13;
A8: (Carrier F) . j = [#] (F . j) by PENCIL_3:7;
y in product (F * a) ;
then y . i in (F * a) . i by GROUP_19:5;
hence (y * (a ")) . j in (Carrier F) . j by A2, A6, A7, A8, FUNCT_1:13; :: thesis: verum
end;
then y * (a ") in product (Carrier F) by A4, A5, CARD_3:def 5;
hence y * (a ") in product F by GROUP_7:def 2; :: thesis: verum