let a be Nat; :: thesis: for r being Real
for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)
let r be Real; :: thesis: for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)
let f be FinSequence of REAL ; :: thesis: (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)
A1: len (f |^ a) = len f by Def1;
A2: len ((f ^ <*r*>) |^ a) = len (f ^ <*r*>) by Def1
.= (len f) + (len <*r*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:40 ;
then A3: dom ((f ^ <*r*>) |^ a) = Seg ((len f) + 1) by FINSEQ_1:def 3;

A4: now :: thesis: for i being Nat st i in dom ((f ^ <*r*>) |^ a) holds
((f ^ <*r*>) |^ a) . i = ((f |^ a) ^ (<*r*> |^ a)) . i

let i be Nat; :: thesis: ( i in dom ((f ^ <*r*>) |^ a) implies ((f ^ <*r*>) |^ a) . b₁ = ((f |^ a) ^ (<*r*> |^ a)) . b₁ )
assume A5: i in dom ((f ^ <*r*>) |^ a) ; :: thesis: ((f ^ <*r*>) |^ a) . b₁ = ((f |^ a) ^ (<*r*> |^ a)) . b₁
A6: 1 <= i by A3, A5, FINSEQ_1:1;
A7: i <= (len f) + 1 by A3, A5, FINSEQ_1:1;

per cases ( i < (len f) + 1 or i = (len f) + 1 ) by A7, XXREAL_0:1;

suppose i < (len f) + 1 ; :: thesis: ((f ^ <*r*>) |^ a) . b₁ = ((f |^ a) ^ (<*r*> |^ a)) . b₁

then A8: i <= len f by NAT_1:13;
then A9: i in dom f by A6, FINSEQ_3:25;
A10: i in dom (f |^ a) by A1, A6, A8, FINSEQ_3:25;
thus ((f ^ <*r*>) |^ a) . i = ((f ^ <*r*>) . i) |^ a by A5, Def1
.= (f . i) |^ a by A9, FINSEQ_1:def 7
.= (f |^ a) . i by A10, Def1
.= ((f |^ a) ^ (<*r*> |^ a)) . i by A10, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose A11: i = (len f) + 1 ; :: thesis: ((f ^ <*r*>) |^ a) . b₁ = ((f |^ a) ^ (<*r*> |^ a)) . b₁

thus ((f ^ <*r*>) |^ a) . i = ((f ^ <*r*>) . i) |^ a by A5, Def1
.= r |^ a by A11, FINSEQ_1:42
.= ((f |^ a) ^ <*(r |^ a)*>) . i by A1, A11, FINSEQ_1:42
.= ((f |^ a) ^ (<*r*> |^ a)) . i by Th12 ; :: thesis: verum

end;

end;

end;

len ((f |^ a) ^ (<*r*> |^ a)) = (len (f |^ a)) + (len (<*r*> |^ a)) by FINSEQ_1:22
.= (len f) + (len (<*r*> |^ a)) by Def1
.= (len f) + (len <*(r |^ a)*>) by Th12
.= (len f) + 1 by FINSEQ_1:40 ;
hence (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) by A2, A4, FINSEQ_2:9; :: thesis: verum