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:36; :: thesis: verum

end;

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

then not k <= len (p ^ q) by FINSEQ_1:35;
then A3: not k in dom (p ^ q) by FINSEQ_3:27;
A4: for n being Element of NAT holds
( n in dom q iff ( 1 <= n & n <= len q ) ) by FINSEQ_3:27;
k - (len p) > len q by A2, XREAL_1:22;
then A5: not k - (len p) in dom q by A4;
thus (p ^ q) . k = {} by A3, FUNCT_1:def 4
.= q . (k - (len p)) by A5, FUNCT_1:def 4 ; :: thesis: verum

end;

end;