let I be non empty set ; :: thesis: for F being Group-Family of I
for x being Element of (product F)
for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}
let F be Group-Family of I; :: thesis: for x being Element of (product F)
for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}
let x be Element of (product F); :: thesis: for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}
let i be Element of I; :: thesis: for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}
let g be Element of (F . i); :: thesis: ( x = (1_ (product F)) +* (i,g) & g <> 1_ (F . i) implies support (x,F) = {i} )
assume that
A1: x = (1_ (product F)) +* (i,g) and
A2: g <> 1_ (F . i) ; :: thesis: support (x,F) = {i}
A3: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by A1, GROUP_12:1;
A4: support (x,F) c= {i} by A1, Th17;
i in support (x,F) by A2, A3, Def1;
then {i} c= support (x,F) by ZFMISC_1:31;
hence support (x,F) = {i} by A4, XBOOLE_0:def 10; :: thesis: verum