deffunc H₁( 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 = H₁(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;