let A1, A2 be V5() ManySortedSubset of X; :: thesis: ( ( for i being Element of I holds A1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) & ( for i being Element of I holds A2 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) implies A1 = A2 )
assume that
A5: for i being Element of I holds A1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } and
A6: for i being Element of I holds A2 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ; :: thesis: A1 = A2
let i be Element of I; :: according to PBOOLE:def 21 :: thesis: A1 . i = A2 . i
thus A1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } by A5
.= A2 . i by A6 ; :: thesis: verum