let n be Nat; :: thesis: for a, b being object
for f being FinSequence st n in dom f holds
n + 2 in dom (<*a,b*> ^ f)
let a, b be object ; :: thesis: for f being FinSequence st n in dom f holds
n + 2 in dom (<*a,b*> ^ f)
let f be FinSequence; :: thesis: ( n in dom f implies n + 2 in dom (<*a,b*> ^ f) )
assume A1: n in dom f ; :: thesis: n + 2 in dom (<*a,b*> ^ f)
A2: 1 <= n by A1, FINSEQ_3:25;
A3: n <= len f by A1, FINSEQ_3:25;
set g = <*a,b*>;
n + 0 <= n + 2 by XREAL_1:6;
then A4: 1 <= n + 2 by A2, XXREAL_0:2;
len <*a,b*> = 2 by FINSEQ_1:44;
then 2 + n <= (len <*a,b*>) + (len f) by A3, XREAL_1:6;
then n + 2 in Seg ((len <*a,b*>) + (len f)) by A4;
hence n + 2 in dom (<*a,b*> ^ f) by FINSEQ_1:def 7; :: thesis: verum