let n be Nat; :: thesis: for p being n -element FinSequence
for q being FinSequence holds (p ^ q) . 1 = p . 1 & ... & (p ^ q) . n = p . n
let p be n -element FinSequence; :: thesis: for q being FinSequence holds (p ^ q) . 1 = p . 1 & ... & (p ^ q) . n = p . n
let q be FinSequence; :: thesis: (p ^ q) . 1 = p . 1 & ... & (p ^ q) . n = p . n
let k be Nat; :: thesis: ( not 1 <= k or not k <= n or (p ^ q) . k = p . k )
A1: len p = n by Th151;
assume ( 1 <= k & k <= n ) ; :: thesis: (p ^ q) . k = p . k
then k in dom p by A1, Th25;
hence (p ^ q) . k = p . k by FINSEQ_1:def 7; :: thesis: verum