let I be non empty set ; :: thesis: for G being Group
for a being finite-support Function of I,G
for i being Element of I
for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds
Product a = g
let G be Group; :: thesis: for a being finite-support Function of I,G
for i being Element of I
for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds
Product a = g
let a be finite-support Function of I,G; :: thesis: for i being Element of I
for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds
Product a = g
let i be Element of I; :: thesis: for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds
Product a = g
let g be Element of G; :: thesis: ( a = (I --> (1_ G)) +* (i,g) implies Product a = g )
assume A1: a = (I --> (1_ G)) +* (i,g) ; :: thesis: Product a = g
A2: dom (I --> (1_ G)) = I by FUNCOP_1:13;

per cases ( g <> 1_ G or g = 1_ G ) ;

suppose A3: g <> 1_ G ; :: thesis: Product a = g

then support a = {i} by A1, Th20;
then i in support a by TARSKI:def 1;
then A6: i in dom (a | (support a)) by FUNCT_2:def 1;
(a | (support a)) * (canFS (support a)) = (a | (support a)) * (canFS {i}) by A1, A3, Th20
.= (a | (support a)) * <*i*> by FINSEQ_1:94
.= <*((a | (support a)) . i)*> by A6, FINSEQ_2:34
.= <*(a . i)*> by A6, FUNCT_1:47
.= <*g*> by A1, A2, FUNCT_7:31 ;
hence Product a = Product <*g*> by GROUP_17:def 1
.= g by GROUP_4:9 ;
:: thesis: verum

end;

suppose A7: g = 1_ G ; :: thesis: Product a = g

a = I --> (1_ G)

proof

A8: dom a = dom (I --> (1_ G)) by A1, FUNCT_7:30;
for j being object st j in I holds
a . j = (I --> (1_ G)) . j

proof

let j be object ; :: thesis: ( j in I implies a . j = (I --> (1_ G)) . j )
assume A9: j in I ; :: thesis: a . j = (I --> (1_ G)) . j
then A10: (I --> (1_ G)) . j = 1_ G by FUNCOP_1:7;

per cases ( j = i or j <> i ) ;

suppose j = i ; :: thesis: a . j = (I --> (1_ G)) . j

hence a . j = (I --> (1_ G)) . j by A1, A2, A7, A10, FUNCT_7:31; :: thesis: verum

end;

suppose j <> i ; :: thesis: a . j = (I --> (1_ G)) . j

then a . j = (I --> (1_ G)) . j by A1, FUNCT_7:32
.= 1_ G by A9, FUNCOP_1:7 ;
hence a . j = (I --> (1_ G)) . j by A9, FUNCOP_1:7; :: thesis: verum

end;

end;

end;

hence a = I --> (1_ G) by A2, A8, FUNCT_1:2; :: thesis: verum

end;

hence Product a = g by A7, Th16; :: thesis: verum

end;

end;