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) holds
support (x,F) c= {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) holds
support (x,F) c= {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) holds
support (x,F) c= {i}
let i be Element of I; :: thesis: for g being Element of (F . i) st x = (1_ (product F)) +* (i,g) holds
support (x,F) c= {i}
let g be Element of (F . i); :: thesis: ( x = (1_ (product F)) +* (i,g) implies support (x,F) c= {i} )
assume A1: x = (1_ (product F)) +* (i,g) ; :: thesis: support (x,F) c= {i}
for j being object st j in support (x,F) holds
j in {i}

proof

let j be object ; :: thesis: ( j in support (x,F) implies j in {i} )
assume j in support (x,F) ; :: thesis: j in {i}
then ex Z being Group st
( Z = F . j & x . j <> 1_ Z & j in I ) by Def1;
then j = i by A1, GROUP_12:1;
hence j in {i} by TARSKI:def 1; :: thesis: verum

end;

hence support (x,F) c= {i} ; :: thesis: verum