let I, J be non empty set ; :: thesis:
let G be Group; :: thesis:
let x be Function of I,G; :: thesis:
let y be Function of J,G; :: thesis:
let a be Function of I,J; :: thesis:
assume that
A1: a is onto and
A2: x = y * a ; :: thesis:
A3: rng a = J by A1, FUNCT_2:def 3;

now :: thesis:

let j be object ; :: thesis:
assume A4: j in support y ; :: thesis:
then consider i being object such that
A5: i in dom a and
A6: j = a . i by A3, FUNCT_1:def 3;
x . i = y . j by A2, A5, A6, FUNCT_1:13;
then x . i <> 1_ G by A4, GROUP_19:def 2;
then i in support x by A5, GROUP_19:def 2;
hence j in a .: (support x) by A5, A6, FUNCT_1:def 6; :: thesis:

end;

then A7: support y c= a .: (support x) ;

now :: thesis:

let j be object ; :: thesis:
assume j in a .: (support x) ; :: thesis:
then consider i being object such that
A8: i in dom a and
A9: i in support x and
A10: j = a . i by FUNCT_1:def 6;
A11: j in J by A8, A10, FUNCT_2:5;
x . i = y . j by A2, A8, A10, FUNCT_1:13;
then y . j <> 1_ G by A9, GROUP_19:def 2;
hence j in support y by A11, GROUP_19:def 2; :: thesis:

end;

then a .: (support x) c= support y ;
hence support y = a .: (support x) by A7, XBOOLE_0:def 10; :: thesis: