let k be non zero Nat; :: thesis: for p being prime odd Nat holds
( (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) & Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) )
let p be prime odd Nat; :: thesis: ( (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) & Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) )
(x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p)

proof

A2: dom (x. (k,p)) = Seg (len (x. (k,p))) by FINSEQ_1:def 3
.= Seg k by Def2 ;
A3: len (x. ((k + 1),p)) = k + 1 by Def2;
then A5: dom (x. ((k + 1),p)) = Seg (k + 1) by FINSEQ_1:def 3;
len ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) = (len (x. (k,p))) + 1 by FINSEQ_2:16
.= k + 1 by Def2 ;
then A6: dom ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) = Seg (k + 1) by FINSEQ_1:def 3;
for i being Nat st i in dom (x. ((k + 1),p)) holds
(x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i

proof

let i be Nat; :: thesis: ( i in dom (x. ((k + 1),p)) implies (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i )
assume i in dom (x. ((k + 1),p)) ; :: thesis: (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i
then i in Seg (k + 1) by A3, FINSEQ_1:def 3;
then i in (Seg k) \/ {(k + 1)} by FINSEQ_1:9;

per cases then ( i in Seg k or i in {(k + 1)} ) by XBOOLE_0:def 3;

suppose A9: i in Seg k ; :: thesis: (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i

k < k + 1 by NAT_1:19;
then Seg k c= Seg (k + 1) by FINSEQ_1:5;
then i in Seg (k + 1) by A9;
then A10: i in dom (x. ((k + 1),p)) by A3, FINSEQ_1:def 3;
((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i = (x. (k,p)) . i by A9, A2, FINSEQ_1:def 7
.= (tau i) |^ p by A9, A2, Def2
.= (x. ((k + 1),p)) . i by A10, Def2 ;
hence (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i ; :: thesis: verum

end;

suppose i in {(k + 1)} ; :: thesis: (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i

then A12: i = k + 1 by TARSKI:def 1;
len (x. (k,p)) = k by Def2;
hence (x. ((k + 1),p)) . i = ((x. (k,p)) ^ <*((tau (k + 1)) |^ p)*>) . i by A12, A5, FINSEQ_1:3, Def2; :: thesis: verum

end;

end;

end;

hence (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) by A5, A6; :: thesis: verum

end;

hence ( (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) & Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) ) by GROUP_4:6; :: thesis: verum