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
proof
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;
hence A = B by A3, A5, FUNCT_2:63; :: thesis: verum