theorem Th19: :: VECTSP11:19

for S being 1-sorted
for F being Function of S,S holds F |^ 1 = F