let p, q be FinSequence; :: thesis: for k being Element of NAT st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))
let k be Element of NAT ; :: thesis: ( (len p) + 1 <= k implies (p ^ q) . k = q . (k - (len p)) )
assume A1: (len p) + 1 <= k ; :: thesis: (p ^ q) . k = q . (k - (len p))

per cases ( k <= (len p) + (len q) or not k <= (len p) + (len q) ) ;

suppose k <= (len p) + (len q) ; :: thesis: (p ^ q) . k = q . (k - (len p))

hence (p ^ q) . k = q . (k - (len p)) by A1, FINSEQ_1:23; :: thesis: verum

end;

suppose A2: not k <= (len p) + (len q) ; :: thesis: (p ^ q) . k = q . (k - (len p))

then k - (len p) > len q by XREAL_1:20;
then A3: not k - (len p) in dom q by FINSEQ_3:25;
not k <= len (p ^ q) by A2, FINSEQ_1:22;
then not k in dom (p ^ q) by FINSEQ_3:25;
hence (p ^ q) . k = {} by FUNCT_1:def 2
.= q . (k - (len p)) by A3, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;