let n, k be Nat; :: thesis: for i1 being Element of n
for p being n + k -element XFinSequence st n <> 0 & k <> 0 holds
(p | n) . i1 = p . i1
let i1 be Element of n; :: thesis: for p being n + k -element XFinSequence st n <> 0 & k <> 0 holds
(p | n) . i1 = p . i1
let p be n + k -element XFinSequence; :: thesis: ( n <> 0 & k <> 0 implies (p | n) . i1 = p . i1 )
assume that
A1: n <> 0 and
A2: k <> 0 ; :: thesis: (p | n) . i1 = p . i1
i1 is Element of Segm n ;
then reconsider I = i1 as Nat ;
k > 0 by A2;
then A3: ( len p = n + k & n + k > n + 0 ) by CARD_1:def 7, XREAL_1:8;
I in n by A1;
hence (p | n) . i1 = p . i1 by A3, AFINSQ_1:53; :: thesis: verum