deffunc H2( 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 = H2(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 V5()
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 b1 being V5() ManySortedSubset of X st
for i being Element of I holds b1 . i = { (nf (x,(R . i))) where x is Element of X . i : verum } by A1, A2; :: thesis: verum