let k, n be Nat; :: thesis: for f being FinSequence st k <= n holds
(f | n) . k = f . k
let f be FinSequence; :: thesis: ( k <= n implies (f | n) . k = f . k )
assume A1: k <= n ; :: thesis: (f | n) . k = f . k

per cases ( k = 0 or 1 <= k ) by NAT_1:14;

suppose A2: k = 0 ; :: thesis: (f | n) . k = f . k

then A3: not k in dom f by Th25;
not k in dom (f | n) by A2, Th25;
hence (f | n) . k = {} by FUNCT_1:def 2
.= f . k by A3, FUNCT_1:def 2 ;
:: thesis: verum

end;

suppose 1 <= k ; :: thesis: (f | n) . k = f . k

then k in Seg n by A1, FINSEQ_1:1;
then (f | (Seg n)) . k = f . k by FUNCT_1:49;
hence (f | n) . k = f . k by FINSEQ_1:def 16; :: thesis: verum

end;

end;