set M = finite-MultiSet_over the carrier of R;
let N1, N2 be strict RelExtension of finite-MultiSet_over the carrier of R; :: thesis: ( ( for m, n being Element of N1 holds
( m <= n iff ex x, y being Element of N1 st
( 1. N1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) ) & ( for m, n being Element of N2 holds
( m <= n iff ex x, y being Element of N2 st
( 1. N2 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) ) implies N1 = N2 )
assume that
A1: for m, n being Element of N1 holds
( m <= n iff ex x, y being Element of N1 st
( 1. N1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) and
A2: for m, n being Element of N2 holds
( m <= n iff ex x, y being Element of N2 st
( 1. N2 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) ; :: thesis: N1 = N2
for m, n being Element of N1
for x, y being Element of N2 st m = x & n = y holds
( m <= n iff x <= y )
proof
let m, n be Element of N1; :: thesis: for x, y being Element of N2 st m = x & n = y holds
( m <= n iff x <= y )
let k, l be Element of N2; :: thesis: ( m = k & n = l implies ( m <= n iff k <= l ) )
assume Z0: m = k ; :: thesis: ( not n = l or ( m <= n iff k <= l ) )
assume Z1: n = l ; :: thesis: ( m <= n iff k <= l )
A5: ( 1. N1 = 1. (finite-MultiSet_over the carrier of R) & 1. (finite-MultiSet_over the carrier of R) = 1. N2 ) by Th3;
hereby :: thesis: ( k <= l implies m <= n )
assume m <= n ; :: thesis: k <= l
then consider x, y being Element of N1 such that
A3: ( 1. N1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A1;
reconsider x = x, y = y as Element of (finite-MultiSet_over the carrier of R) by Th2;
reconsider x = x, y = y as Element of N2 by Th2;
( 1. N2 <> x & x divides l & k = (l -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by Z0, Z1, A3, A5;
hence k <= l by A2; :: thesis: verum
end;
assume k <= l ; :: thesis: m <= n
then consider x, y being Element of N2 such that
A4: ( 1. N2 <> x & x divides l & k = (l -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by A2;
reconsider x = x, y = y as Element of (finite-MultiSet_over the carrier of R) by Th2;
reconsider x = x, y = y as Element of N1 by Th2;
( 1. N1 <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) by Z0, Z1, A4, A5;
hence m <= n by A1; :: thesis: verum
end;
hence N1 = N2 by Th4; :: thesis: verum