let I be non empty set ; 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; 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 ; 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; 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; ( 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)) )
; 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
; verum