let i be Nat; :: thesis: for p, q being FinSequence st len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) holds
(p ^ q) . i = q . (i - (len p))
let p, q be FinSequence; :: thesis: ( len p < i & ( i <= (len p) + (len q) or i <= len (p ^ q) ) implies (p ^ q) . i = q . (i - (len p)) )
assume that
A1: len p < i and
A2: ( i <= (len p) + (len q) or i <= len (p ^ q) ) ; :: thesis: (p ^ q) . i = q . (i - (len p))
i <= (len p) + (len q) by A2, FINSEQ_1:22;
then A3: i - (len p) <= ((len p) + (len q)) - (len p) by XREAL_1:9;
(len p) + 1 <= i by A1, NAT_1:13;
then A4: ((len p) + 1) - (len p) <= i - (len p) by XREAL_1:9;
then A5: (len p) + (i -' (len p)) = (len p) + (i - (len p)) by XREAL_0:def 2
.= i ;
i - (len p) = i -' (len p) by A4, XREAL_0:def 2;
then i -' (len p) in dom q by A4, A3, FINSEQ_3:25;
hence (p ^ q) . i = q . (i - (len p)) by A5, FINSEQ_1:def 7; :: thesis: verum