:: deftheorem Def3 defines LAG4SQg LAGRA4SQ:def 4 :
for v being Nat
for b₂ being FinSequence of INT holds
( b₂ = LAG4SQg v iff ( len b₂ = v & ( for i being Nat st i in dom b₂ holds
b₂ . i = (- 1) - ((i - 1) ^2) ) ) );