let x be set ; :: according to VALUED_0:def 11 :: thesis: ( not x in proj1 (f1 (#) f2) or (f1 (#) f2) . x is integer )
assume x in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . x is integer
then (f1 (#) f2) . x = (f1 . x) * (f2 . x) by Def4;
hence (f1 (#) f2) . x is integer ; :: thesis: verum