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 ( len p < k & k <= len (p ^ q) ) ; :: thesis: (p ^ q) . k = q . (k - (len p))
then ( (len p) + 1 <= k & k <= (len p) + (len q) ) by Th22, NAT_1:13;
hence (p ^ q) . k = q . (k - (len p)) by Th23; :: thesis: verum