let G be Group; :: thesis: for a being FinSequence of G st ( for i being object st i in dom a holds
a . i = 1_ G ) holds
Product a = 1_ G
let a be FinSequence of G; :: thesis: ( ( for i being object st i in dom a holds
a . i = 1_ G ) implies Product a = 1_ G )
assume A1: for i being object st i in dom a holds
a . i = 1_ G ; :: thesis: Product a = 1_ G
set n = len a;
a = (len a) |-> (1_ G)
proof
(len a) |-> (1_ G) = (Seg (len a)) --> (1_ G) by FINSEQ_2:def 2;
then A2: dom ((len a) |-> (1_ G)) = Seg (len a) by FUNCOP_1:13;
A3: dom a = Seg (len a) by FINSEQ_1:def 3;
for i being object st i in dom a holds
a . i = ((len a) |-> (1_ G)) . i
proof
let i be object ; :: thesis: ( i in dom a implies a . i = ((len a) |-> (1_ G)) . i )
assume A4: i in dom a ; :: thesis: a . i = ((len a) |-> (1_ G)) . i
then i in Seg (len a) by FINSEQ_1:def 3;
then ((len a) |-> (1_ G)) . i = 1_ G by FINSEQ_2:57;
hence a . i = ((len a) |-> (1_ G)) . i by A1, A4; :: thesis: verum
end;
hence a = (len a) |-> (1_ G) by A2, A3, FUNCT_1:2; :: thesis: verum
end;
then Product a = (1_ G) |^ (len a) by GROUP_4:12
.= 1_ G by GROUP_1:31 ;
hence Product a = 1_ G ; :: thesis: verum