deffunc H1( Real) -> set = (2 * $1)- 1; deffunc H2( Real) -> set = $1 -(1 / 4); deffunc H3( Real) -> set = (1 / 2)* $1; defpred S1[ Real] means $1 > 3 / 4; defpred S2[ Real] means ( $1 > 1 / 2 & $1 <= 3 / 4 ); defpred S3[ Real] means $1 <= 1 / 2; A1:
for c being Element of I[01] holds ( S3[c] or S2[c] or S1[c] )
; A2:
for c being Element of I[01] holds ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) )
byXXREAL_0:2; consider f being Function such that A3:
( dom f = the carrier of I[01] & ( for c being Element of I[01] holds ( ( S3[c] implies f . c = H3(c) ) & ( S2[c] implies f . c = H2(c) ) & ( S1[c] implies f . c = H1(c) ) ) ) )
fromBORSUK_6:sch 1(A2, A1);
for x being object st x in the carrier of I[01] holds f . x in the carrier of I[01]