let p, q be FinSequence; :: thesis: for k being Nat st (len p) + 1 <= k & k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
let k be Nat; :: thesis: ( (len p) + 1 <= k & k <= (len p) + (len q) implies (p ^ q) . k = q . (k - (len p)) )
assume A1: ( (len p) + 1 <= k & k <= (len p) + (len q) ) ; :: thesis: (p ^ q) . k = q . (k - (len p))
then consider m being Nat such that
A2: ((len p) + 1) + m = k by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A3: (len p) + (1 + m) = k by A2;
1 + m = k - (len p) by A2;
then A4: 1 <= 1 + m by A1, XREAL_1:21;
k - (len p) <= len q by A1, XREAL_1:22;
then 1 + m in Seg (len q) by A2, A4;
then 1 + m in dom q by Def3;
hence (p ^ q) . k = q . (k - (len p)) by A3, Def7; :: thesis: verum