let A, B be strict NetStr over 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 #) 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 ) ; :: 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, A5;

for c being Element of C holds f1 . c = f2 . c

( 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 ) ; :: 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, A5;

for c being Element of C holds f1 . c = f2 . c

proof

hence
A = B
by A3, A5, FUNCT_2:63; :: thesis: verum
let c be Element of C; :: thesis: f1 . c = f2 . c

( ex ya being Element of L st

( ya = the mapping of N . c & f1 . c = x "/\" ya ) & ex yb being Element of L st

( yb = the mapping of N . c & f2 . c = x "/\" yb ) ) by A3, A4, A5, A6;

hence f1 . c = f2 . c ; :: thesis: verum

end;( ex ya being Element of L st

( ya = the mapping of N . c & f1 . c = x "/\" ya ) & ex yb being Element of L st

( yb = the mapping of N . c & f2 . c = x "/\" yb ) ) by A3, A4, A5, A6;

hence f1 . c = f2 . c ; :: thesis: verum