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

(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