thus F * f is Function-yielding :: thesis: verum

proof

let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( x in dom (F * f) implies (F * f) . x is Function )
assume x in dom (F * f) ; :: thesis: (F * f) . x is Function
then (F * f) . x = F . (f . x) by FUNCT_1:12;
hence (F * f) . x is Function ; :: thesis: verum

end;