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 that
A1: (len p) + 1 <= k and
A2: k <= (len p) + (len q) ; :: thesis: (p ^ q) . k = q . (k - (len p))
consider m being Nat such that
A3: ((len p) + 1) + m = k by A1, NAT_1:10;
A4: (len p) + (1 + m) = k by A3;
1 + m = k - (len p) by A3;
then A5: 1 <= 1 + m by A1, XREAL_1:19;
k - (len p) <= len q by A2, XREAL_1:20;
then 1 + m in Seg (len q) by A3, A5;
then 1 + m in dom q by Def3;
hence (p ^ q) . k = q . (k - (len p)) by A4, Def7; :: thesis: verum