let A, B be strict NetStr over L; ( RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of A ex y being Element of L st
( y = the mapping of N . i & the mapping of A . i = x "/\" y ) ) & RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #) & ( for i being Element of B ex y being Element of L st
( y = the mapping of N . i & the mapping of B . i = x "/\" y ) ) implies A = B )
assume that
A3:
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of N, the InternalRel of N #)
and
A4:
for i being Element of A ex y being Element of L st
( y = the mapping of N . i & the mapping of A . i = x "/\" y )
and
A5:
RelStr(# the carrier of B, the InternalRel of B #) = RelStr(# the carrier of N, the InternalRel of N #)
and
A6:
for i being Element of B ex y being Element of L st
( y = the mapping of N . i & the mapping of B . i = x "/\" y )
; A = B
reconsider C = the carrier of A as non empty set by A3;
reconsider f1 = the mapping of A, f2 = the mapping of B as Function of C, the carrier of L by A3, A5;
for c being Element of C holds f1 . c = f2 . c
hence
A = B
by A3, A5, FUNCT_2:63; verum