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):],the carrier of T by A4, A6;

now

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:9;
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:113; :: thesis: verum