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