deffunc H₁( object ) -> Element of bool (J . (In ($1,I))) = support ((x | (J . (In ($1,I)))),(F . (In ($1,I))));
consider sz being Function such that
A1: ( dom sz = I & ( for i being object st i in I holds
sz . i = H₁(i) ) ) from FUNCT_1:sch 3();
reconsider sz = sz as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;
A2: for i being Element of I holds sz . i = support ((x | (J . i)),(F . i))

proof

let i be Element of I; :: thesis: sz . i = support ((x | (J . i)),(F . i))
In (i,I) = i ;
hence sz . i = support ((x | (J . i)),(F . i)) by A1; :: thesis: verum

end;

A3: J is disjoint_valued ;
for i, j being object st i <> j holds
sz . i misses sz . j

proof

let i, j be object ; :: thesis: ( i <> j implies sz . i misses sz . j )
assume A4: i <> j ; :: thesis: sz . i misses sz . j

per cases ( not i in dom sz or not j in dom sz or ( i in dom sz & j in dom sz ) ) ;

suppose ( not i in dom sz or not j in dom sz ) ; :: thesis: sz . i misses sz . j

then ( sz . i = {} or sz . j = {} ) by FUNCT_1:def 2;
then (sz . i) /\ (sz . j) = {} ;
hence sz . i misses sz . j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose ( i in dom sz & j in dom sz ) ; :: thesis: sz . i misses sz . j

then reconsider i = i, j = j as Element of I ;
A6: ( sz . i = support ((x | (J . i)),(F . i)) & sz . j = support ((x | (J . j)),(F . j)) ) by A2;
A7: (sz . i) /\ (sz . j) c= (J . i) /\ (J . j) by A6, XBOOLE_1:27;
(J . i) /\ (J . j) = {} by A3, A4, XBOOLE_0:def 7;
then (sz . i) /\ (sz . j) = {} by A7;
hence sz . i misses sz . j by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

then sz is disjoint_valued ;
then reconsider sz = sz as disjoint_valued ManySortedSet of I ;
take sz ; :: thesis: for i being Element of I holds sz . i = support ((x | (J . i)),(F . i))
thus for i being Element of I holds sz . i = support ((x | (J . i)),(F . i)) by A2; :: thesis: verum