set T = TOP-REAL 0 ;
let x be Element of the carrier of [:(TOP-REAL 0 ),(TOP-REAL 0 ):]; :: according to FUNCT_2:def 9 :: thesis: (TIMES 0 ) . x = ([:(TOP-REAL 0 ),(TOP-REAL 0 ):] --> (0. (TOP-REAL 0 ))) . x
thus (TIMES 0 ) . x = ([:(TOP-REAL 0 ),(TOP-REAL 0 ):] --> (0. (TOP-REAL 0 ))) . x ; :: thesis: verum