let p, q be FinSequence; :: thesis: for i being Nat st 1 <= i & i <= len q holds
(p ^ q) . ((len p) + i) = q . i
let i be Nat; :: thesis: ( 1 <= i & i <= len q implies (p ^ q) . ((len p) + i) = q . i )
assume ( 1 <= i & i <= len q ) ; :: thesis: (p ^ q) . ((len p) + i) = q . i
then ( (len p) + 1 <= (len p) + i & (len p) + i <= (len p) + (len q) ) by XREAL_1:6;
hence (p ^ q) . ((len p) + i) = q . (((len p) + i) - (len p)) by Th23
.= q . i ;
:: thesis: verum