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