let f be Real_Sequence; :: thesis: for k, n being Nat st k in Seg n holds
(f |_ (Seg n)) . k = f . k
let k, n be Nat; :: thesis: ( k in Seg n implies (f |_ (Seg n)) . k = f . k )
assume A0: k in Seg n ; :: thesis: (f |_ (Seg n)) . k = f . k
A1: dom f = NAT by FUNCT_2:def 1;
dom (f | (Seg n)) = Seg n by A1, RELAT_1:62;
then (f |_ (Seg n)) . k = (f | (Seg n)) . k by A0, FUNCT_4:13
.= f . k by A0, FUNCT_1:49 ;
hence (f |_ (Seg n)) . k = f . k ; :: thesis: verum