thus (0RFunctional V) . (0. V) = 0 by FUNCOP_1:7; :: according to HAHNBAN1:def 15 :: thesis: verum