let e be Element of sproduct f; :: thesis: e is f -compatible
let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in dom e or e . x in f . x )
assume x in dom e ; :: thesis: e . x in f . x
hence e . x in f . x by Th65; :: thesis: verum