deffunc H_{1}( object ) -> set = proj (f,$1);

consider g being ManySortedSet of dom f such that

A1: for x being object st x in dom f holds

g . x = H_{1}(x)
from PBOOLE:sch 4();

take g ; :: thesis: for x being object st x in dom f holds

g . x = proj (f,x)

thus for x being object st x in dom f holds

g . x = proj (f,x) by A1; :: thesis: verum

consider g being ManySortedSet of dom f such that

A1: for x being object st x in dom f holds

g . x = H

now :: thesis: for x being object st x in dom g holds

g . x is Function

then reconsider g = g as ManySortedFunction of dom f by FUNCOP_1:def 6;g . x is Function

let x be object ; :: thesis: ( x in dom g implies g . x is Function )

assume x in dom g ; :: thesis: g . x is Function

then g . x = proj (f,x) by A1;

hence g . x is Function ; :: thesis: verum

end;assume x in dom g ; :: thesis: g . x is Function

then g . x = proj (f,x) by A1;

hence g . x is Function ; :: thesis: verum

take g ; :: thesis: for x being object st x in dom f holds

g . x = proj (f,x)

thus for x being object st x in dom f holds

g . x = proj (f,x) by A1; :: thesis: verum