deffunc H₁( object ) -> Element of omega = (b1 . $1) -' (b2 . $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 x being object holds f . x = (b1 . x) -' (b2 . x)
let x be object ; :: thesis: f . x = (b1 . x) -' (b2 . x)

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: f . x = (b1 . x) -' (b2 . x)

hence f . x = (b1 . x) -' (b2 . x) by A1; :: thesis: verum

end;

suppose A2: not x in X ; :: thesis: f . x = (b1 . x) -' (b2 . x)

A3: dom b2 = X by PARTFUN1:def 2;
A4: dom b1 = X by PARTFUN1:def 2;
dom f = X by PARTFUN1:def 2;
hence f . x = 0 by A2, FUNCT_1:def 2
.= 0 -' 0 by XREAL_1:232
.= 0 -' (b2 . x) by A2, A3, FUNCT_1:def 2
.= (b1 . x) -' (b2 . x) by A2, A4, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;