deffunc H₁( object ) -> Element of S . $1 = the Element of S . $1;
consider f being ManySortedSet of I such that
A1: for x being object st x in I holds
f . x = H₁(x) from PBOOLE:sch 4();
take f ; :: thesis: for i being set st i in I holds
f . i is Element of S . i
let x be set ; :: thesis: ( x in I implies f . x is Element of S . x )
assume x in I ; :: thesis: f . x is Element of S . x
then f . x = H₁(x) by A1;
hence f . x is Element of S . x ; :: thesis: verum