let IT1, IT2 be strict net of T; :: thesis:
assume that
A4: RelStr(# the carrier of IT1, the InternalRel of IT1 #) = [:Y,(product J):] and
A5: for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT1 . (i,f) = the mapping of (J . i) . (f . i) and
A6: RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [:Y,(product J):] and
A7: for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of IT2 . (i,f) = the mapping of (J . i) . (f . i) ; :: thesis:
the carrier of RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [: the carrier of Y, the carrier of (product J):] by A6, YELLOW_3:def 2;
then reconsider m1 = the mapping of IT1, m2 = the mapping of IT2 as Function of [: the carrier of Y, the carrier of (product J):],T by A4, A6;

let c be Element of [: the carrier of Y, the carrier of (product J):]; :: thesis:
consider c1 being Element of Y, c2 being Element of (product J) such that
A8: c = [c1,c2] by DOMAIN_1:1;
reconsider d = c2 as Element of product (Carrier J) by YELLOW_1:def 4;
thus m1 . c = m1 . (c1,d) by A8
.= the mapping of (J . c1) . (d . c1) by A5
.= m2 . (c1,d) by A7
.= m2 . c by A8 ; :: thesis:

end;