let I be non empty set ; :: thesis:
let F be Group-Family of I; :: thesis:
let i be Element of I; :: thesis:
let a, b be Function; :: thesis:
assume that
A2: dom a = I and
A3: b = a +* (i,(1_ (F . i))) ; :: thesis:
for j being object holds
( j in support (b,F) iff j in (support (a,F)) \ {i} )

let j be object ; :: thesis:

end;

assume j in (support (a,F)) \ {i} ; :: thesis:
then A10: ( j in support (a,F) & not j in {i} ) by XBOOLE_0:def 5;
then consider Z being Group such that
A: ( Z = F . j & a . j <> 1_ Z & j in I ) by Def1;
{j} misses {i} by A10, ZFMISC_1:50;
then b . j = a . j by A3, FUNCT_7:32;
hence j in support (b,F) by A, Def1; :: thesis:

end;