let I be set ; :: thesis: for A being ManySortedSet of ex B being V8() ManySortedSet of st A c= B
let A be ManySortedSet of ; :: thesis: ex B being V8() ManySortedSet of st A c= B
deffunc H₁( set ) -> set = {{} } \/ (A . $1);
consider f being ManySortedSet of such that
A1: for i being set st i in I holds
f . i = H₁(i) from PBOOLE:sch 4();
f is non-empty

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not f . i is empty )
assume i in I ; :: thesis: not f . i is empty
then f . i = {{} } \/ (A . i) by A1;
hence not f . i is empty ; :: thesis: verum

end;

then reconsider f = f as V8() ManySortedSet of ;
take f ; :: thesis: A c= f
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= f . i )
assume i in I ; :: thesis: A . i c= f . i
then f . i = (A . i) \/ {{} } by A1;
hence A . i c= f . i by XBOOLE_1:7; :: thesis: verum