let I be non empty set ; :: thesis: for F being Group-Family of I
for x being Function
for i being Element of I
for g being Element of (F . i) st support (x,F) is finite holds
support ((x +* (i,g)),F) is finite
let F be Group-Family of I; :: thesis: for x being Function
for i being Element of I
for g being Element of (F . i) st support (x,F) is finite holds
support ((x +* (i,g)),F) is finite
let x be Function; :: thesis: for i being Element of I
for g being Element of (F . i) st support (x,F) is finite holds
support ((x +* (i,g)),F) is finite
let i be Element of I; :: thesis: for g being Element of (F . i) st support (x,F) is finite holds
support ((x +* (i,g)),F) is finite
let g be Element of (F . i); :: thesis: ( support (x,F) is finite implies support ((x +* (i,g)),F) is finite )
reconsider y = x +* (i,g) as Function ;
assume A1: support (x,F) is finite ; :: thesis: support ((x +* (i,g)),F) is finite
for j being object st j in support (y,F) holds
j in (support (x,F)) \/ {i}
proof
let j be object ; :: thesis: ( j in support (y,F) implies j in (support (x,F)) \/ {i} )
assume j in support (y,F) ; :: thesis: j in (support (x,F)) \/ {i}
then A2: ex Z being Group st
( Z = F . j & y . j <> 1_ Z & j in I ) by Def1;
per cases ( j = i or j <> i ) ;
end;
end;
then support (y,F) c= (support (x,F)) \/ {i} ;
hence support ((x +* (i,g)),F) is finite by A1; :: thesis: verum