let e be Element of sproduct f; :: thesis: e is I -defined
A: dom f c= I by RELAT_1:def 18;
dom e c= dom f by Th65;
hence dom e c= I by A, XBOOLE_1:1; :: according to RELAT_1:def 18 :: thesis: verum