let e be Element of product f; :: thesis: e is I -defined
dom f c= I by RELAT_1:def 18;
hence dom e c= I by Th18; :: according to RELAT_1:def 18 :: thesis: verum