theorem Th25: :: EUCLID_7:26

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