for v being Nat holds LAG4SQf v is one-to-one