deffunc H₁( set ) -> Element of REAL = a * (b . $1);
consider f being ManySortedSet of X such that
A1: for i being set st i in X holds
f . i = H₁(i) from PBOOLE:sch 4();
take f ; :: thesis: for i being set holds f . i = a * (b . i)
let i be set ; :: 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 4;
dom f = X by PARTFUN1:def 4;
hence f . i = a * 0 by A2, FUNCT_1:def 4
.= a * (b . i) by A2, A3, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;