:: deftheorem Def15 defines TriangleShift2 NUMBER17:def 15 :
for n, a being Nat st n >= a + 1 holds
for b₃ being FinSequence of NAT holds
( b₃ = TriangleShift2 (n,a) iff ( len b₃ = (n - a) - 1 & ( for i being Nat st 1 <= i & i <= len b₃ holds
b₃ . i = Triangle (a + i) ) ) );