let I be non empty set ; :: thesis:
let G be Group; :: thesis:
let a be finite-support Function of I,G; :: thesis:
let W be finite Subset of I; :: thesis:
assume A1: support a c= W ; :: thesis:
A2: for i being object holds
( i in support a iff i in support (a | W) )

let i be object ; :: thesis:

hereby :: thesis:

assume A3: i in support a ; :: thesis:
then A4: ( a . i <> 1_ G & i in I ) by Def2;
(a | W) . i = a . i by A1, A3, FUNCT_1:49;
hence i in support (a | W) by A1, A3, A4, Def2; :: thesis:

end;

assume A6: i in support (a | W) ; :: thesis:
then A7: ( (a | W) . i <> 1_ G & i in W ) by Def2;
(a | W) . i = a . i by A6, FUNCT_1:49;
hence i in support a by A7, Def2; :: thesis:

end;

support (a | W) is finite ;
then reconsider aW = a | W as finite-support Function of W,G by Def3;
take aW ; :: thesis:
aW | (support aW) = (a | W) | (support a) by A2, TARSKI:2
.= a | (support a) by A1, RELAT_1:74 ;
hence ( aW = a | W & support a = support aW & Product a = Product aW ) by A2, TARSKI:2; :: thesis: