let I be non empty set ; :: thesis: for F being Group-Family of I
for i being Element of I
for a being Element of (sum F)
for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1
let F be Group-Family of I; :: thesis: for i being Element of I
for a being Element of (sum F)
for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1
let i be Element of I; :: thesis: for a being Element of (sum F)
for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1
let a be Element of (sum F); :: thesis: for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1
let b be Function; :: thesis: ( i in support (a,F) & b = a +* (i,(1_ (F . i))) implies card (support (b,F)) = (card (support (a,F))) - 1 )
assume that
A1: i in support (a,F) and
A2: b = a +* (i,(1_ (F . i))) ; :: thesis: card (support (b,F)) = (card (support (a,F))) - 1
a is Element of (product F) by GROUP_2:42;
then dom a = I by Th3;
then support (b,F) = (support (a,F)) \ {i} by A2, Th27;
then card (support (b,F)) = (card (support (a,F))) - (card {i}) by A1, CARD_2:44, ZFMISC_1:31
.= (card (support (a,F))) - 1 by CARD_2:42 ;
hence card (support (b,F)) = (card (support (a,F))) - 1 ; :: thesis: verum