:: deftheorem Def3 defines FuncsSeq TRIANG_1:def 3 :
for X, b₂ being SetSequence holds
( b₂ = FuncsSeq X iff for n being Nat holds b₂ . n = Funcs ((X . (n + 1)),(X . n)) );