let I be set ; :: thesis: for G being Group
for x being finite-support Function of I,G st support x = {} holds
Product x = 1_ G
let G be Group; :: thesis: for x being finite-support Function of I,G st support x = {} holds
Product x = 1_ G
let x be finite-support Function of I,G; :: thesis: ( support x = {} implies Product x = 1_ G )
assume support x = {} ; :: thesis: Product x = 1_ G
then (x | (support x)) * (canFS (support x)) = <*> the carrier of G ;
then Product (x | (support x)) = Product (<*> the carrier of G) by GROUP_17:def 1
.= 1_ G by GROUP_4:8 ;
hence Product x = 1_ G ; :: thesis: verum