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