theorem NormIn01: :: FUZNORM1:15

for a, b being Real
for t being BinOp of [.0,1.] holds t . (a,b) in [.0,1.]