deffunc H2( object ) -> set = {I};
consider S being ManySortedSet of I such that
A1: for x being object st x in I holds
S . x = H2(x) from PBOOLE:sch 4();
 take S ; :: thesis: ( S is V5() & S is V276() )
hereby :: according to PBOOLE:def 13 :: thesis: S is V276()
let x be object ; :: thesis: ( x in I implies not S . x is empty )
assume x in I ; :: thesis: not S . x is empty
then S . x = H2(x) by A1;
hence not S . x is empty ; :: thesis: verum
end;
let x be set ; :: according to MSAFREE4:def 2 :: thesis: ( x in I implies S . x is trivial )
assume x in I ; :: thesis: S . x is trivial
then S . x = H2(x) by A1;
hence S . x is trivial ; :: thesis: verum