let I be non empty set ; :: thesis: for G being Group
for i being object
for a being finite-support Function of I,G
for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card (support b) = (card (support a)) - 1
let G be Group; :: thesis: for i being object
for a being finite-support Function of I,G
for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card (support b) = (card (support a)) - 1
let i be object ; :: thesis: for a being finite-support Function of I,G
for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card (support b) = (card (support a)) - 1
let a be finite-support Function of I,G; :: thesis: for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card (support b) = (card (support a)) - 1
let b be Function of I,G; :: thesis: ( i in support a & b = a +* (i,(1_ G)) implies card (support b) = (card (support a)) - 1 )
assume A1: ( i in support a & b = a +* (i,(1_ G)) ) ; :: thesis: card (support b) = (card (support a)) - 1
then support b = (support a) \ {i} by Th28;
then card (support b) = (card (support a)) - (card {i}) by A1, CARD_2:44, ZFMISC_1:31
.= (card (support a)) - 1 by CARD_2:42 ;
hence card (support b) = (card (support a)) - 1 ; :: thesis: verum