let k be Element of NAT ; :: thesis: for q, p being XFinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
let q, p be XFinSequence; :: 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 Element of NAT st
( n = k & (len p) + n in dom (p ^ q) ) by Th25;
hence (len p) + k in dom (p ^ q) ; :: thesis: verum