deffunc H_{1}( 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_{1}(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_{1}(x)
by A1;

hence f . x is Element of S . x ; :: thesis: verum

consider f being ManySortedSet of I such that

A1: for x being object st x in I holds

f . x = H

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

hence f . x is Element of S . x ; :: thesis: verum