let p, q be FinSequence; :: thesis: for k being Nat st len p < k & k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
let k be Nat; :: 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 A2: (len p) + 1 <= k by NAT_1:13;
k <= (len p) + (len q) by A1, Th35;
hence (p ^ q) . k = q . (k - (len p)) by A2, Th36; :: thesis: verum