let f be FinSequence of REAL ; :: thesis: f |^ 0 = (len f) |-> 1
A1: len (f |^ 0) = len f by Def1;
A2: 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:25;
A5: k in Seg (len f) by A1, A3;
thus (f |^ 0) . k = (f . k) |^ 0 by A4, Def1
.= 1 by NEWTON:4
.= ((len f) |-> 1) . k by A5, FUNCOP_1:7 ; :: thesis: verum

end;

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