let e be Element of product f; :: thesis: e is f -compatible
let x be object ; :: according to FUNCT_1:def 14 :: thesis: ( not x in proj1 e or e . x in f . x )
assume x in dom e ; :: thesis: e . x in f . x
then x in dom f by Th9;
hence e . x in f . x by Th9; :: thesis: verum