let I be non empty set ; 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; 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 ; 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; ( 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))
; 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} )
hence
support b = (support a) \ {i}
by TARSKI:2; verum