let i be Nat; :: thesis: for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i
let p, q be XFinSequence; :: thesis: (p ^ q) /^ ((len p) + i) = q /^ i
A1: len (p ^ q) = (len p) + (len q) by AFINSQ_1:17;

per cases ( i < len q or i >= len q ) ;

suppose A2: i < len q ; :: thesis: (p ^ q) /^ ((len p) + i) = q /^ i

then (len p) + i < (len p) + (len q) by XREAL_1:6;
then (len p) + i < len (p ^ q) by AFINSQ_1:17;
then A3: len ((p ^ q) /^ ((len p) + i)) = (len (p ^ q)) - ((len p) + i) by Th7
.= ((len q) + (len p)) - ((len p) + i) by AFINSQ_1:17
.= (len q) - i
.= len (q /^ i) by A2, Th7 ;

now :: thesis: for k being Nat st k < len (q /^ i) holds
((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k

let k be Nat; :: thesis: ( k < len (q /^ i) implies ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k )
assume A4: k < len (q /^ i) ; :: thesis: ((p ^ q) /^ ((len p) + i)) . k = (q /^ i) . k
then A5: k in dom (q /^ i) by AFINSQ_1:86;
k < (len q) - i by A2, A4, Th7;
then A6: i + k in dom q by AFINSQ_1:86, XREAL_1:20;
k in dom ((p ^ q) /^ ((len p) + i)) by A3, A4, AFINSQ_1:86;
hence ((p ^ q) /^ ((len p) + i)) . k = (p ^ q) . (((len p) + i) + k) by Def2
.= (p ^ q) . ((len p) + (i + k))
.= q . (i + k) by A6, AFINSQ_1:def 3
.= (q /^ i) . k by A5, Def2 ;
:: thesis: verum

end;

hence (p ^ q) /^ ((len p) + i) = q /^ i by A3, AFINSQ_1:9; :: thesis: verum

end;

suppose A7: i >= len q ; :: thesis: (p ^ q) /^ ((len p) + i) = q /^ i

hence (p ^ q) /^ ((len p) + i) = {} by Th6, A1, XREAL_1:6
.= q /^ i by A7, Th6 ;
:: thesis: verum

end;

end;