deffunc H1( 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 = H1(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))
A3:
J is disjoint_valued
;
for i, j being object st i <> j holds
sz . i misses sz . j
then
sz is disjoint_valued
;
then reconsider sz = sz as disjoint_valued ManySortedSet of I ;
take
sz
; 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; verum