set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
let it1, it2 be non empty strict NetStr over L; :: thesis: ( the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it1 holds it1 . i = i `1 ) & the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it2 holds it2 . i = i `1 ) implies it1 = it2 )
assume that
A6: the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f } and
A7: for i, j being Element of it1 holds
( i <= j iff j `2 c= i `2 ) and
A8: for i being Element of it1 holds it1 . i = i `1 and
A9: the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f } and
A10: for i, j being Element of it2 holds
( i <= j iff j `2 c= i `2 ) and
A11: for i being Element of it2 holds it2 . i = i `1 ; :: thesis: it1 = it2
A12: for x, y being object holds
( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )

proof

let x, y be object ; :: thesis: ( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 )

hereby :: thesis: ( [x,y] in the InternalRel of it2 implies [x,y] in the InternalRel of it1 )

assume A13: [x,y] in the InternalRel of it1 ; :: thesis: [x,y] in the InternalRel of it2
then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it2 by A6, A9, A13, ZFMISC_1:87;
i <= j by A13, ORDERS_2:def 5;
then j9 `2 c= i9 `2 by A7;
then i9 <= j9 by A10;
hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5; :: thesis: verum

end;

assume A14: [x,y] in the InternalRel of it2 ; :: thesis: [x,y] in the InternalRel of it1
then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it1 by A6, A9, A14, ZFMISC_1:87;
i <= j by A14, ORDERS_2:def 5;
then j9 `2 c= i9 `2 by A10;
then i9 <= j9 by A7;
hence [x,y] in the InternalRel of it1 by ORDERS_2:def 5; :: thesis: verum

end;

the mapping of it1 = the mapping of it2

proof

reconsider f2 = the mapping of it2 as Function of { [a,f] where a is Element of L, f is Element of F : a in f } , the carrier of L by A9;
reconsider f1 = the mapping of it1 as Function of { [a,f] where a is Element of L, f is Element of F : a in f } , the carrier of L by A6;
for x being object st x in { [a,f] where a is Element of L, f is Element of F : a in f } holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in { [a,f] where a is Element of L, f is Element of F : a in f } implies f1 . x = f2 . x )
assume A15: x in { [a,f] where a is Element of L, f is Element of F : a in f } ; :: thesis: f1 . x = f2 . x
then reconsider x1 = x as Element of it1 by A6;
reconsider x2 = x as Element of it2 by A9, A15;
reconsider x = x as Element of { [a,f] where a is Element of L, f is Element of F : a in f } by A15;
f1 . x = it1 . x1
.= x1 `1 by A8
.= it2 . x2 by A11 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence the mapping of it1 = the mapping of it2 by FUNCT_2:12; :: thesis: verum

end;

hence it1 = it2 by A6, A9, A12, RELAT_1:def 2; :: thesis: verum