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

proof

let j be object ; :: thesis: ( j in support (b,F) iff j in (support (a,F)) \ {i} )

hereby :: thesis: ( j in (support (a,F)) \ {i} implies j in support (b,F) )

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

end;

assume j in (support (a,F)) \ {i} ; :: thesis: j in support (b,F)
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: verum

end;

hence support (b,F) = (support (a,F)) \ {i} by TARSKI:2; :: thesis: verum