let i be Nat; :: thesis: for f, g being XFinSequence holds (f ^ g) /^ ((len f) + i) = g /^ i
let f, g be XFinSequence; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i
A1: len (f ^ g) = (len f) + (len g) by AFINSQ_1:20;

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

suppose A2: i < len g ; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i

then (len f) + i < (len f) + (len g) by XREAL_1:8;
then (len f) + i < len (f ^ g) by AFINSQ_1:20;
then A3: len ((f ^ g) /^ ((len f) + i)) = (len (f ^ g)) - ((len f) + i) by TH80b
.= ((len g) + (len f)) - ((len f) + i) by AFINSQ_1:20
.= (len g) - i
.= len (g /^ i) by A2, TH80b ;

now

let k be Element of NAT ; :: thesis: ( k < len (g /^ i) implies ((f ^ g) /^ ((len f) + i)) . k = (g /^ i) . k )
assume A4: k < len (g /^ i) ; :: thesis: ((f ^ g) /^ ((len f) + i)) . k = (g /^ i) . k
then A5: k in dom (g /^ i) by NAT_1:45;
k < (len g) - i by A2, A4, TH80b;
then i + k < len g by XREAL_1:22;
then A6: i + k in dom g by NAT_1:45;
k in dom ((f ^ g) /^ ((len f) + i)) by A3, A4, NAT_1:45;
hence ((f ^ g) /^ ((len f) + i)) . k = (f ^ g) . (((len f) + i) + k) by Def2
.= (f ^ g) . ((len f) + (i + k))
.= g . (i + k) by A6, AFINSQ_1:def 4
.= (g /^ i) . k by A5, Def2 ;
:: thesis: verum

end;

hence (f ^ g) /^ ((len f) + i) = g /^ i by A3, AFINSQ_1:11; :: thesis: verum

end;

suppose A7: i >= len g ; :: thesis: (f ^ g) /^ ((len f) + i) = g /^ i

then (len f) + i >= len (f ^ g) by A1, XREAL_1:8;
hence (f ^ g) /^ ((len f) + i) = {} by TH80e
.= g /^ i by A7, TH80e ;
:: thesis: verum

end;

end;