let a, n be Nat; :: thesis: ( a + 1 <= n implies TriangleShift2 (n,a) is triangular-valued )
set f = TriangleShift2 (n,a);
assume A1: a + 1 <= n ; :: thesis: TriangleShift2 (n,a) is triangular-valued
let x be object ; :: according to NUMBER06:def 8 :: thesis: (TriangleShift2 (n,a)) . x is triangular

per cases ( x in dom (TriangleShift2 (n,a)) or not x in dom (TriangleShift2 (n,a)) ) ;

suppose A2: x in dom (TriangleShift2 (n,a)) ; :: thesis: (TriangleShift2 (n,a)) . x is triangular

then reconsider x = x as Nat ;
( 1 <= x & x <= len (TriangleShift2 (n,a)) ) by A2, FINSEQ_3:25;
then (TriangleShift2 (n,a)) . x = Triangle (a + x) by A1, Def15;
hence (TriangleShift2 (n,a)) . x is triangular ; :: thesis: verum

end;

suppose not x in dom (TriangleShift2 (n,a)) ; :: thesis: (TriangleShift2 (n,a)) . x is triangular

hence (TriangleShift2 (n,a)) . x is triangular by FUNCT_1:def 2; :: thesis: verum

end;

end;