set T = TOP-REAL 0;
let x be Element of the carrier of [:(TOP-REAL 0),(TOP-REAL 0):]; :: according to FUNCT_2:def 8 :: 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