let k be Element of 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 A1: ( len p <= k & k < (len p) + (len q) ) ; :: thesis: (p ^ q) . k = q . (k - (len p))
then consider m being Nat such that
A2: (len p) + m = k by NAT_1:10;
k - (len p) < ((len p) + (len q)) - (len p) by A1, XREAL_1:16;
then m in dom q by A2, NAT_1:45;
hence (p ^ q) . k = q . (k - (len p)) by A2, Def4; :: thesis: verum