let I be non empty set ; :: thesis: for G being Group
for a being finite-support Function of I,G st a = I --> (1_ G) holds
Product a = 1_ G
let G be Group; :: thesis: for a being finite-support Function of I,G st a = I --> (1_ G) holds
Product a = 1_ G
let a be finite-support Function of I,G; :: thesis: ( a = I --> (1_ G) implies Product a = 1_ G )
assume a = I --> (1_ G) ; :: thesis: Product a = 1_ G
then support a is empty by Th12;
hence Product a = 1_ G by Th15; :: thesis: verum