let f be FinSequence; :: thesis: for n being Nat holds (f ^ <*0*>) . n = f . n
let n be Nat; :: thesis: (f ^ <*0*>) . n = f . n
reconsider g = <*0*> as FinSequence ;

per cases ( n in dom f or not n in dom f ) ;

suppose n in dom f ; :: thesis: (f ^ <*0*>) . n = f . n

hence (f ^ <*0*>) . n = f . n by FINSEQ_1:def 7; :: thesis: verum

end;

suppose not n in dom f ; :: thesis: (f ^ <*0*>) . n = f . n

then ( n < 1 or len f < n ) by FINSEQ_3:25;

per cases then ( n = 0 or n > len f ) by NAT_1:14;

suppose n = 0 ; :: thesis: (f ^ <*0*>) . n = f . n

hence (f ^ <*0*>) . n = f . n ; :: thesis: verum

end;

suppose n > len f ; :: thesis: (f ^ <*0*>) . n = f . n

then n - (len f) > (len f) - (len f) by XREAL_1:9;
then reconsider m = n - (len f) as non zero Nat ;
(f ^ g) . ((len f) + m) = g . m by FINSEQ165
.= 0 ;
hence (f ^ <*0*>) . n = f . n ; :: thesis: verum

end;

end;

end;

end;