theorem Th20: :: INTEGRA8:20

for L1 being LinearFunc holds - L1 is LinearFunc