let A, B be strict NetStr of L; :: thesis: ( 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 #) & ( 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
A4: ( 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 ) ) ) ; :: thesis: 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, A4;
for c being Element of C holds f1 . c = f2 . c

proof

let c be Element of C; :: thesis: f1 . c = f2 . c
consider ya being Element of L such that
A5: ( ya = the mapping of N . c & f1 . c = x "/\" ya ) by A3;
consider yb being Element of L such that
A6: ( yb = the mapping of N . c & f2 . c = x "/\" yb ) by A3, A4;
thus f1 . c = f2 . c by A5, A6; :: thesis: verum

end;

hence A = B by A3, A4, FUNCT_2:113; :: thesis: verum