let a be natural number ; :: 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 ^ <*r*>) |^ a) = len (f ^ <*r*>) by Def1
.= (len f) + (len <*r*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:57 ;
A2: len ((f |^ a) ^ (<*r*> |^ a)) = (len (f |^ a)) + (len (<*r*> |^ a)) by FINSEQ_1:35
.= (len f) + (len (<*r*> |^ a)) by Def1
.= (len f) + (len <*(r |^ a)*>) by Th12
.= (len f) + 1 by FINSEQ_1:57 ;
A3: len (f |^ a) = len f by Def1;
X: dom ((f ^ <*r*>) |^ a) = Seg ((len f) + 1) by A1, FINSEQ_1:def 3;

now

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

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

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

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

end;

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

thus ((f ^ <*r*>) |^ a) . i = ((f ^ <*r*>) . i) |^ a by A6, Def1
.= r |^ a by A10, FINSEQ_1:59
.= ((f |^ a) ^ <*(r |^ a)*>) . i by A3, A10, FINSEQ_1:59
.= ((f |^ a) ^ (<*r*> |^ a)) . i by Th12 ; :: thesis: verum

end;

end;

end;

hence (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) by A1, A2, FINSEQ_2:10; :: thesis: verum