let n be Nat; :: thesis: for p, q being FinSequence st 1 <= n & n <= len q holds
q . n = (p ^ q) . ((len p) + n)
let p, q 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:25;
hence q . n = (p ^ q) . ((len p) + n) by FINSEQ_1:def 7; :: thesis: verum