deffunc H1( 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 = H1(x) from PBOOLE:sch 4();
now :: thesis: for x being object st x in dom g holds
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;
then reconsider g = g as ManySortedFunction of dom f by FUNCOP_1:def 6;
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