theorem lem1: :: LAGRA4SQ:2

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