let G be Group; :: thesis: for F being FinSequence of the carrier of G holds F |^ ((len F) |-> (@ 0 )) = (len F) |-> (1_ G)
let F be FinSequence of the carrier of G; :: thesis: F |^ ((len F) |-> (@ 0 )) = (len F) |-> (1_ G)
defpred S₁[ FinSequence of the carrier of G] means $1 |^ ((len $1) |-> (@ 0 )) = (len $1) |-> (1_ G);
A1: S₁[ <*> the carrier of G]

proof

set A = <*> the carrier of G;
thus (<*> the carrier of G) |^ ((len (<*> the carrier of G)) |-> (@ 0 )) = (<*> the carrier of G) |^ (0 |-> (@ 0 ))
.= (<*> the carrier of G) |^ (<*> INT ) by FINSEQ_2:72
.= {} by Th27
.= (len (<*> the carrier of G)) |-> (1_ G) by FINSEQ_2:72 ; :: thesis: verum

end;

A2: for F being FinSequence of the carrier of G
for a being Element of G st S₁[F] holds
S₁[F ^ <*a*>]

proof

let F be FinSequence of the carrier of G; :: thesis: for a being Element of G st S₁[F] holds
S₁[F ^ <*a*>]
let a be Element of G; :: thesis: ( S₁[F] implies S₁[F ^ <*a*>] )
set A = F ^ <*a*>;
assume A3: S₁[F] ; :: thesis: S₁[F ^ <*a*>]
A4: len (F ^ <*a*>) = (len F) + (len <*a*>) by FINSEQ_1:35;
A5: len <*a*> = 1 by FINSEQ_1:57;
A6: len <*(@ 0 )*> = 1 by FINSEQ_1:57;
A7: len ((len F) |-> (@ 0 )) = len F by FINSEQ_1:def 18;
thus (F ^ <*a*>) |^ ((len (F ^ <*a*>)) |-> (@ 0 )) = (F ^ <*a*>) |^ (((len F) |-> (@ 0 )) ^ <*(@ 0 )*>) by A4, A5, FINSEQ_2:74
.= (F |^ ((len F) |-> (@ 0 ))) ^ (<*a*> |^ <*(@ 0 )*>) by A5, A6, A7, Th25
.= ((len F) |-> (1_ G)) ^ <*(a |^ 0 )*> by A3, Th28
.= ((len F) |-> (1_ G)) ^ <*(1_ G)*> by GROUP_1:43
.= (len (F ^ <*a*>)) |-> (1_ G) by A4, A5, FINSEQ_2:74 ; :: thesis: verum

end;

for F being FinSequence of the carrier of G holds S₁[F] from FINSEQ_2:sch 2(A1, A2);
hence F |^ ((len F) |-> (@ 0 )) = (len F) |-> (1_ G) ; :: thesis: verum