deffunc H₁( set ) -> set = b2 . $1;
deffunc H₂( set ) -> set = b1 . $1;
defpred S₁[ set ] means b1 . $1 <= b2 . $1;
consider f being ManySortedSet of X such that
A1: for i being Element of X st i in X holds
( ( S₁[i] implies f . i = H₂(i) ) & ( not S₁[i] implies f . i = H₁(i) ) ) from PRE_CIRC:sch 2();
take f ; :: thesis: for i being object holds
( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) )
let i be object ; :: thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) )

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

suppose i in X ; :: thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) )

hence ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) by A1; :: thesis: verum

end;

suppose A2: not i in X ; :: thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) )

then not i in dom f by PARTFUN1:def 2;
then A3: f . i = 0 by FUNCT_1:def 2;
( not i in dom b1 & not i in dom b2 ) by A2, PARTFUN1:def 2;
hence ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) by A3, FUNCT_1:def 2; :: thesis: verum

end;

end;