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