for i, n being Nat holds sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i)