let n be Nat; :: thesis: for G being Group
for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)
let G be Group; :: thesis: for I being FinSequence of INT st len I = n holds
(n |-> (1_ G)) |^ I = n |-> (1_ G)
let I be FinSequence of INT ; :: thesis: ( len I = n implies (n |-> (1_ G)) |^ I = n |-> (1_ G) )
defpred S₁[ Nat] means for I being FinSequence of INT st len I = $1 holds
($1 |-> (1_ G)) |^ I = $1 |-> (1_ G);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
let I be FinSequence of INT ; :: thesis: ( len I = k + 1 implies ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G) )
reconsider J = I | (Seg k) as FinSequence of INT by FINSEQ_1:18;
assume A3: len I = k + 1 ; :: thesis: ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G)
then A4: len J = k by FINSEQ_3:53;
then A5: (k |-> (1_ G)) |^ J = k |-> (1_ G) by A2;
A6: rng I c= INT by FINSEQ_1:def 4;
1 <= k + 1 by NAT_1:12;
then k + 1 in dom I by A3, FINSEQ_3:25;
then I . (k + 1) in rng I by FUNCT_1:def 3;
then reconsider i = I . (k + 1) as Integer by A6;
A7: ( len <*(1_ G)*> = 1 & len <*(@ i)*> = 1 ) by FINSEQ_1:40;
A8: ( (k + 1) |-> (1_ G) = (k |-> (1_ G)) ^ <*(1_ G)*> & len (k |-> (1_ G)) = k ) by CARD_1:def 7, FINSEQ_2:60;
I = J ^ <*(@ i)*> by A3, FINSEQ_3:55;
then ((k + 1) |-> (1_ G)) |^ I = ((k |-> (1_ G)) |^ J) ^ (<*(1_ G)*> |^ <*(@ i)*>) by A4, A8, A7, Th19
.= (k |-> (1_ G)) ^ <*((1_ G) |^ i)*> by A5, Th22
.= (k |-> (1_ G)) ^ <*(1_ G)*> by GROUP_1:31 ;
hence ((k + 1) |-> (1_ G)) |^ I = (k + 1) |-> (1_ G) by FINSEQ_2:60; :: thesis: verum

end;

A9: S₁[ 0 ]

proof

let I be FinSequence of INT ; :: thesis: ( len I = 0 implies (0 |-> (1_ G)) |^ I = 0 |-> (1_ G) )
assume len I = 0 ; :: thesis: (0 |-> (1_ G)) |^ I = 0 |-> (1_ G)
then A10: I = <*> INT ;
{} = <*> the carrier of G ;
hence (0 |-> (1_ G)) |^ I = 0 |-> (1_ G) by A10, Th21; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A1);
hence ( len I = n implies (n |-> (1_ G)) |^ I = n |-> (1_ G) ) ; :: thesis: verum