let m, n be Nat; :: thesis: for p being n -element FinSequence
for q being m -element FinSequence holds (p ^ q) . (n + 1) = q . 1 & ... & (p ^ q) . (n + m) = q . m
let p be n -element FinSequence; :: thesis: for q being m -element FinSequence holds (p ^ q) . (n + 1) = q . 1 & ... & (p ^ q) . (n + m) = q . m
let q be m -element FinSequence; :: thesis: (p ^ q) . (n + 1) = q . 1 & ... & (p ^ q) . (n + m) = q . m
A1: len p = n by Th151;
A2: len q = m by Th151;
let k be Nat; :: thesis: ( not 1 <= k or not k <= m or (p ^ q) . (n + k) = q . k )
assume ( 1 <= k & k <= m ) ; :: thesis: (p ^ q) . (n + k) = q . k
then A3: ( n + 1 <= n + k & n + k <= n + m ) by XREAL_1:6;
thus (p ^ q) . (n + k) = (p ^ q) . (n + k)
.= q . ((n + k) - n) by A3, A1, A2, FINSEQ_1:23
.= q . k ; :: thesis: verum