deffunc H1( set ) -> set = b1 . $1;
deffunc H2( set ) -> set = b2 . $1;
defpred S1[ 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
( ( S1[i] implies f . i = H2(i) ) & ( not S1[i] implies f . i = H1(i) ) )
from PRE_CIRC:sch 2();
take
f
; for i being object holds
( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) )
let i be object ; ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) )
per cases
( i in X or not i in X )
;
suppose
i in X
;
( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) )hence
( (
b1 . i <= b2 . i implies
f . i = b2 . i ) & (
b1 . i > b2 . i implies
f . i = b1 . i ) )
by A1;
verum end; suppose A2:
not
i in X
;
( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) )end; end;