let I, J be non empty set ; :: thesis:
let G be Group; :: thesis:
let x be finite-support Function of I,G; :: thesis:
let y be finite-support Function of J,G; :: thesis:
let a be Function of I,J; :: thesis:
assume that
A1: a is bijective and
A2: x = y * a and
A3: for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i) ; :: thesis:
reconsider rx = rng x as non empty Subset of G ;
reconsider ry = rng y as non empty Subset of G ;
A4: dom y = J by FUNCT_2:def 1;
A5: rng a = J by A1, FUNCT_2:def 3;
A6: gr rx = gr ry by A2, A4, A5, RELAT_1:28;
rng x c= [#] (gr rx) by GROUP_4:def 4;
then reconsider x1 = x as finite-support Function of I,(gr rx) by GROUP_20:5;
rng y c= [#] (gr ry) by GROUP_4:def 4;
then reconsider y1 = y as finite-support Function of J,(gr rx) by A6, GROUP_20:5;

let a, b be Element of G; :: thesis:
assume that
A7: a in rx and
A8: b in rx ; :: thesis:
consider i being object such that
A9: i in dom x and
A10: a = x . i by A7, FUNCT_1:def 3;
consider j being object such that
A11: j in dom x and
A12: b = x . j by A8, FUNCT_1:def 3;
reconsider i = i as Element of I by A9;
reconsider j = j as Element of I by A11;
(x . i) * (x . j) = (x . j) * (x . i) by A3;
hence a * b = b * a by A10, A12; :: thesis:

end;