deffunc H₂( Element of I) -> set = { (nf (x,(R . $1))) where x is Element of X . $1 : verum } ;
consider A being ManySortedSet of I such that
A1: for i being Element of I holds A . i = H₂(i) from PBOOLE:sch 5();
A2: A is ManySortedSubset of X

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or A . i c= X . i )
assume i in I ; :: thesis: A . i c= X . i
then reconsider j = i as Element of I ;
A3: A . j = { (nf (x,(R . j))) where x is Element of X . j : verum } by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in X . i )
assume x in A . i ; :: thesis: x in X . i
then ex y being Element of X . j st x = nf (y,(R . j)) by A3;
hence x in X . i ; :: thesis: verum

end;

A is non-empty

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not A . i is empty )
assume i in I ; :: thesis: not A . i is empty
then reconsider j = i as Element of I ;
A4: A . j = { (nf (x,(R . j))) where x is Element of X . j : verum } by A1;
set x = the Element of X . j;
nf ( the Element of X . j,(R . j)) in A . i by A4;
hence not A . i is empty ; :: thesis: verum

end;

hence ex b₁ being non-empty ManySortedSubset of X st
for i being Element of I holds b₁ . i = { (nf (x,(R . i))) where x is Element of X . i : verum } by A1, A2; :: thesis: verum