let I be non empty set ; :: thesis: for G being Group
for x being finite-support Function of I,G st ( for i being object st i in I holds
x . i = 1_ G ) holds
Product x = 1_ G
let G be Group; :: thesis: for x being finite-support Function of I,G st ( for i being object st i in I holds
x . i = 1_ G ) holds
Product x = 1_ G
let x be finite-support Function of I,G; :: thesis: ( ( for i being object st i in I holds
x . i = 1_ G ) implies Product x = 1_ G )
assume A1: for i being object st i in I holds
x . i = 1_ G ; :: thesis: Product x = 1_ G
support x = {}
proof
assume not support x = {} ; :: thesis: contradiction
then consider i being object such that
A2: i in support x by XBOOLE_0:def 1;
( x . i <> 1_ G & i in I ) by A2, GROUP_19:def 2;
hence contradiction by A1; :: thesis: verum
end;
hence Product x = 1_ G by GROUP_19:15; :: thesis: verum