let R be non empty transitive asymmetric RelStr ; :: thesis: for a, b being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x
let a, b be bag of the carrier of R; :: thesis: for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x
let x be Element of R; :: thesis: for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x
let p be partition of b -' a; :: thesis: for q being partition of b st q is ordered & q = <*a*> ^ p & a . x > 0 holds
a . x = b . x
let q be partition of b; :: thesis: ( q is ordered & q = <*a*> ^ p & a . x > 0 implies a . x = b . x )
assume Z0: q is ordered ; :: thesis: ( not q = <*a*> ^ p or not a . x > 0 or a . x = b . x )
assume Z1: q = <*a*> ^ p ; :: thesis: ( not a . x > 0 or a . x = b . x )
assume Z2: a . x > 0 ; :: thesis: a . x = b . x
( a in {a} & {a} = rng <*a*> ) by TARSKI:def 1, FINSEQ_1:39;
then ( a in (rng <*a*>) \/ (rng p) & (rng <*a*>) \/ (rng p) = rng q ) by Z1, XBOOLE_0:def 3, FINSEQ_1:31;
hence a . x = b . x by Z0, Z2; :: thesis: verum