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 S1[ FinSequence of the carrier of G] means $1 |^ ((len $1) |-> (@ 0)) = (len $1) |-> (1_ G);
A1: for F being FinSequence of the carrier of G
for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
proof
let F be FinSequence of the carrier of G; :: thesis: for a being Element of G st S1[F] holds
S1[F ^ <*a*>]
let a be Element of G; :: thesis: ( S1[F] implies S1[F ^ <*a*>] )
set A = F ^ <*a*>;
assume A2: S1[F] ; :: thesis: S1[F ^ <*a*>]
A3: len <*a*> = 1 by FINSEQ_1:40;
A4: ( len <*(@ 0)*> = 1 & len ((len F) |-> (@ 0)) = len F ) by CARD_1:def 7;
A5: len (F ^ <*a*>) = (len F) + (len <*a*>) by FINSEQ_1:22;
hence (F ^ <*a*>) |^ ((len (F ^ <*a*>)) |-> (@ 0)) = (F ^ <*a*>) |^ (((len F) |-> (@ 0)) ^ <*(@ 0)*>) by A3, FINSEQ_2:60
.= (F |^ ((len F) |-> (@ 0))) ^ (<*a*> |^ <*(@ 0)*>) by A3, A4, Th19
.= ((len F) |-> (1_ G)) ^ <*(a |^ 0)*> by A2, Th22
.= ((len F) |-> (1_ G)) ^ <*(1_ G)*> by GROUP_1:25
.= (len (F ^ <*a*>)) |-> (1_ G) by A5, A3, FINSEQ_2:60 ;
:: thesis: verum
end;
A6: S1[ <*> 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 Th21
.= (len (<*> the carrier of G)) |-> (1_ G) ; :: thesis: verum
end;
for F being FinSequence of the carrier of G holds S1[F] from FINSEQ_2:sch 2(A6, A1);
 hence F |^ ((len F) |-> (@ 0)) = (len F) |-> (1_ G) ; :: thesis: verum