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

proof

let i be object ; :: according to PBOOLE:def 13 :: 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 non-empty ManySortedSet of I ;
take f ; :: thesis: A c= f
let i be object ; :: according to PBOOLE:def 2 :: 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