thus (0Functional V) . (0. V) = 0. K by FUNCOP_1:7; :: according to HAHNBAN1:def 9 :: thesis: verum