deffunc H1( object ) -> set = a * (b . $1);
consider f being ManySortedSet of X such that
A1: for i being object st i in X holds
f . i = H1(i) from PBOOLE:sch 4();
 take f ; :: thesis: for i being object holds f . i = a * (b . i)
let i be object ; :: thesis: f . i = a * (b . i)
per cases ( i in X or not i in X ) ;
suppose i in X ; :: thesis: f . i = a * (b . i)
hence f . i = a * (b . i) by A1; :: thesis: verum
end;
suppose A2: not i in X ; :: thesis: f . i = a * (b . i)
A3: dom b = X by PARTFUN1:def 2;
dom f = X by PARTFUN1:def 2;
hence f . i = a * 0 by A2, FUNCT_1:def 2
.= a * (b . i) by A2, A3, FUNCT_1:def 2 ;
:: thesis: verum
end;
end;