let f be FinSequence of REAL ; :: thesis: f |^ 1 = f
A1: for k being Nat st 1 <= k & k <= len (f |^ 1) holds
(f |^ 1) . k = f . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (f |^ 1) implies (f |^ 1) . k = f . k )
assume ( 1 <= k & k <= len (f |^ 1) ) ; :: thesis: (f |^ 1) . k = f . k
then k in dom (f |^ 1) by FINSEQ_3:25;
hence (f |^ 1) . k = (f . k) |^ 1 by Def1
.= f . k ;
:: thesis: verum

end;

len (f |^ 1) = len f by Def1;
hence f |^ 1 = f by A1; :: thesis: verum