let n be non zero Nat; :: thesis: for f, g being FinSequence holds (f ^ g) . ((len f) + n) = g . n
let f, g be FinSequence; :: thesis: (f ^ g) . ((len f) + n) = g . n

per cases ( n in dom g or not n in dom g ) ;

suppose n in dom g ; :: thesis: (f ^ g) . ((len f) + n) = g . n

hence (f ^ g) . ((len f) + n) = g . n by FINSEQ_1:def 7; :: thesis: verum

end;

suppose B1: not n in dom g ; :: thesis: (f ^ g) . ((len f) + n) = g . n

then ( n < 1 or len g < n ) by FINSEQ_3:25;
then (len f) + (len g) < (len f) + n by NAT_1:14, XREAL_1:6;
then len (f ^ g) < (len f) + n by FINSEQ_1:22;
then not (len f) + n in dom (f ^ g) by FINSEQ_3:25;
then (f ^ g) . ((len f) + n) = 0 by FUNCT_1:def 2;
hence (f ^ g) . ((len f) + n) = g . n by B1, FUNCT_1:def 2; :: thesis: verum

end;

end;