theorem lem2: :: LAGRA4SQ:3

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