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 )

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

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

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;hereby :: thesis: ( [x,y] in the InternalRel of it2 implies [x,y] in the InternalRel of it1 )

assume A14:
[x,y] in the InternalRel of it2
; :: thesis: [x,y] in the InternalRel of it1assume 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;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

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

proof

hence
it1 = it2
by A6, A9, A12, RELAT_1:def 2; :: thesis: verum
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

end;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

hence
the mapping of it1 = the mapping of it2
by FUNCT_2:12; :: thesis: verum
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;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