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

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