let k be 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 that
A1: len p <= k and
A2: k < len (p ^ q) ; :: thesis: (p ^ q) . k = q . (k - (len p))
k < (len p) + (len q) by A2, Def3;
hence (p ^ q) . k = q . (k - (len p)) by A1, Th16; :: thesis: verum