let k be Nat; :: thesis: for p, q being XFinSequence st len p <= k & k < (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
let p, q be XFinSequence; :: thesis: ( len p <= k & k < (len p) + (len q) implies (p ^ q) . k = q . (k - (len p)) )
assume that
A1: len p <= 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) + m = k by A1, NAT_1:10;
k - (len p) < ((len p) + (len q)) - (len p) by A2, XREAL_1:14;
then m in dom q by A3, Lm1;
hence (p ^ q) . k = q . (k - (len p)) by A3, Def3; :: thesis: verum