let I be non empty set ; :: thesis: for G being Group
for i being object
for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
support b = (support a) \ {i}
let G be Group; :: thesis: for i being object
for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
support b = (support a) \ {i}
let i be object ; :: thesis: for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
support b = (support a) \ {i}
let a, b be Function of I,G; :: thesis: ( i in support a & b = a +* (i,(1_ G)) implies support b = (support a) \ {i} )
assume that
A1: i in support a and
A2: b = a +* (i,(1_ G)) ; :: thesis: support b = (support a) \ {i}
A4: dom a = I by FUNCT_2:def 1;
A5: b . i = 1_ G by A1, A2, A4, FUNCT_7:31;
for j being object holds
( j in support b iff j in (support a) \ {i} )
proof
let j be object ; :: thesis: ( j in support b iff j in (support a) \ {i} )
hereby :: thesis: ( j in (support a) \ {i} implies j in support b )
assume j in support b ; :: thesis: j in (support a) \ {i}
then A7: ( b . j <> 1_ G & j in I ) by Def2;
then {j} misses {i} by A5, ZFMISC_1:11;
then A9: not j in {i} by ZFMISC_1:48;
a . j = b . j by A2, A5, A7, FUNCT_7:32;
then j in support a by A7, Def2;
hence j in (support a) \ {i} by A9, XBOOLE_0:def 5; :: thesis: verum
end;
assume j in (support a) \ {i} ; :: thesis: j in support b
then A10: ( j in support a & not j in {i} ) by XBOOLE_0:def 5;
{j} misses {i} by A10, ZFMISC_1:50;
then A11: b . j = a . j by A2, FUNCT_7:32;
( a . j <> 1_ G & j in I ) by A10, Def2;
hence j in support b by A11, Def2; :: thesis: verum
end;
hence support b = (support a) \ {i} by TARSKI:2; :: thesis: verum