let n be Element of NAT ; :: thesis: for q, p being FinSequence st 1 <= n & n <= len q holds
q . n = (p ^ q) . ((len p) + n)
let q, p be FinSequence; :: thesis: ( 1 <= n & n <= len q implies q . n = (p ^ q) . ((len p) + n) )
assume ( 1 <= n & n <= len q ) ; :: thesis: q . n = (p ^ q) . ((len p) + n)
then n in dom q by FINSEQ_3:27;
hence q . n = (p ^ q) . ((len p) + n) by FINSEQ_1:def 7; :: thesis: verum