let f be FinSequence of REAL ; :: thesis: f |^ 0 = (len f) |-> 1
A1: len (f |^ 0 ) = len f by Def1;
A2: len ((len f) |-> 1) = len f by FINSEQ_1:def 18;
for k being Nat st 1 <= k & k <= len (f |^ 0 ) holds
(f |^ 0 ) . k = ((len f) |-> 1) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (f |^ 0 ) implies (f |^ 0 ) . k = ((len f) |-> 1) . k )
assume A3: ( 1 <= k & k <= len (f |^ 0 ) ) ; :: thesis: (f |^ 0 ) . k = ((len f) |-> 1) . k
then A4: k in dom (f |^ 0 ) by FINSEQ_3:27;
then A5: k in Seg (len f) by A1, A3;
thus (f |^ 0 ) . k = (f . k) |^ 0 by A4, Def1
.= 1 by NEWTON:9
.= ((len f) |-> 1) . k by A5, FUNCOP_1:13 ; :: thesis: verum

end;

hence f |^ 0 = (len f) |-> 1 by A1, A2, FINSEQ_1:18; :: thesis: verum