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