let f1, f2 be disjoint_valued ManySortedSet of I; :: thesis: ( ( for i being Element of I holds f1 . i = support ((x | (J . i)),(F . i)) ) & ( for i being Element of I holds f2 . i = support ((x | (J . i)),(F . i)) ) implies f1 = f2 )
assume that
A8: for i being Element of I holds f1 . i = support ((x | (J . i)),(F . i)) and
A9: for i being Element of I holds f2 . i = support ((x | (J . i)),(F . i)) ; :: thesis: f1 = f2
A10: dom f1 = I by PARTFUN1:def 2;
for i being object st i in dom f1 holds
f1 . i = f2 . i

proof

let i be object ; :: thesis: ( i in dom f1 implies f1 . i = f2 . i )
assume i in dom f1 ; :: thesis: f1 . i = f2 . i
then reconsider i0 = i as Element of I ;
thus f1 . i = support ((x | (J . i)),(F . i0)) by A8
.= f2 . i by A9 ; :: thesis: verum

end;

hence f1 = f2 by A10, PARTFUN1:def 2; :: thesis: verum