let I be finite set ; :: thesis: for G being Group
for a being I -defined the carrier of b₁ -valued total Function st ( for i being object st i in I holds
a . i = 1_ G ) holds
Product a = 1_ G
let G be Group; :: thesis: for a being I -defined the carrier of G -valued total Function st ( for i being object st i in I holds
a . i = 1_ G ) holds
Product a = 1_ G
let a be I -defined the carrier of G -valued total Function; :: thesis: ( ( for i being object st i in I holds
a . i = 1_ G ) implies Product a = 1_ G )
assume A1: for i being object st i in I holds
a . i = 1_ G ; :: thesis: Product a = 1_ G
set cs = canFS I;
set acs = a * (canFS I);
A2: rng (a * (canFS I)) c= the carrier of G ;
A3: ( I = dom a & rng (canFS I) = I ) by FUNCT_2:def 3, PARTFUN1:def 2;
then dom (a * (canFS I)) = dom (canFS I) by RELAT_1:27;
then dom (a * (canFS I)) = Seg (len (canFS I)) by FINSEQ_1:def 3;
then a * (canFS I) is FinSequence by FINSEQ_1:def 2;
then reconsider acs = a * (canFS I) as FinSequence of G by A2, FINSEQ_1:def 4;
A4: Product a = Product acs by GROUP_17:def 1;
for i being object st i in dom acs holds
acs . i = 1_ G

proof

let i be object ; :: thesis: ( i in dom acs implies acs . i = 1_ G )
assume A5: i in dom acs ; :: thesis: acs . i = 1_ G
then i in dom (canFS I) by A3, RELAT_1:27;
then (canFS I) . i in rng (canFS I) by FUNCT_1:3;
then a . ((canFS I) . i) = 1_ G by A1;
hence acs . i = 1_ G by A5, FUNCT_1:12; :: thesis: verum

end;

hence Product a = 1_ G by A4, Th48; :: thesis: verum