let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (a * b) or (a * b) . x is real )
assume x in dom (a * b) ; :: thesis: (a * b) . x is real
(a * b) . x = a * (b . x) by Def2;
then (a * b) . x is real ;
hence (a * b) . x is real ; :: thesis: verum