let I be non empty set ; :: thesis: for F being Group-Family of I
for i being object
for a, b being Function st i in I & 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 object
for a, b being Function st i in I & dom a = I & b = a +* (i,(1_ (F . i))) holds
support (b,F) = (support (a,F)) \ {i}
let i be object ; :: thesis: for a, b being Function st i in I & dom a = I & b = a +* (i,(1_ (F . i))) holds
support (b,F) = (support (a,F)) \ {i}
let a, b be Function; :: thesis: ( i in I & dom a = I & b = a +* (i,(1_ (F . i))) implies support (b,F) = (support (a,F)) \ {i} )
assume that
A1: i in I and
A2: dom a = I and
A3: b = a +* (i,(1_ (F . i))) ; :: thesis: support (b,F) = (support (a,F)) \ {i}
A5: b . i = 1_ (F . i) by A1, A2, A3, FUNCT_7:31;
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 A7: j in support (b,F) ; :: thesis: j in (support (a,F)) \ {i}
then A8: j <> i by A5, Def1;
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 ( a . j <> 1_ (F . j) & j in I ) by A7, Def1;
then j in support (a,F) by 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;
{j} misses {i} by A10, ZFMISC_1:50;
then A11: b . j = a . j by A3, FUNCT_7:32;
( a . j <> 1_ (F . j) & j in I ) by A10, Def1;
hence j in support (b,F) by A11, Def1; :: thesis: verum

end;

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