let IT1, IT2 be strict net of T; :: thesis: ( RelStr(# the carrier of IT1, the InternalRel of IT1 #) = [:Y,(product J):] & ( 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) ) & RelStr(# the carrier of IT2, the InternalRel of IT2 #) = [:Y,(product J):] & ( 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) ) implies IT1 = IT2 )
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: IT1 = IT2
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;

now :: thesis: for c being Element of [: the carrier of Y, the carrier of (product J):] holds m1 . c = m2 . c

let c be Element of [: the carrier of Y, the carrier of (product J):]; :: thesis: m1 . c = m2 . c
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: verum

end;

hence IT1 = IT2 by A4, A6, FUNCT_2:63; :: thesis: verum