let k be Nat; :: thesis: for p, q being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
let p, q be FinSequence; :: thesis: ( k in dom q implies (len p) + k in dom (p ^ q) )
assume k in dom q ; :: thesis: (len p) + k in dom (p ^ q)
then ex n being Nat st
( n = k & (len p) + n in dom (p ^ q) ) by Th27;
hence (len p) + k in dom (p ^ q) ; :: thesis: verum