let k be Element of NAT ; :: thesis: for p, q being XFinSequence st len p <= k & k < len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
let p, q be XFinSequence; :: thesis: ( len p <= k & k < len (p ^ q) implies (p ^ q) . k = q . (k - (len p)) )
assume A1: ( len p <= k & k < len (p ^ q) ) ; :: thesis: (p ^ q) . k = q . (k - (len p))
then k < (len p) + (len q) by Def4;
hence (p ^ q) . k = q . (k - (len p)) by A1, Th21; :: thesis: verum