set C = [.0,1.];

defpred S_{1}[ set , set ] means ( $1 = 1 or $2 = 1 );

deffunc H_{1}( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((min ($1,$2)),[.0,1.]);

deffunc H_{2}( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In (0,[.0,1.]);

ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st

for c, d being Element of [.0,1.] st [c,d] in dom f holds

( ( S_{1}[c,d] implies f . [c,d] = H_{1}(c,d) ) & ( not S_{1}[c,d] implies f . [c,d] = H_{2}(c,d) ) )
from SCHEME1:sch 21();

then consider f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] such that

A1: for c, d being Element of [.0,1.] st [c,d] in dom f holds

( ( S_{1}[c,d] implies f . [c,d] = H_{1}(c,d) ) & ( not S_{1}[c,d] implies f . [c,d] = H_{2}(c,d) ) )
;

take f ; :: thesis: for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

A0: dom f = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;

let a, b be Element of [.0,1.]; :: thesis: ( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

cc: ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

AA: [a,b] in dom f by A0, ZFMISC_1:87;

( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

defpred S

deffunc H

deffunc H

ex f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] st

for c, d being Element of [.0,1.] st [c,d] in dom f holds

( ( S

then consider f being Function of [:[.0,1.],[.0,1.]:],[.0,1.] such that

A1: for c, d being Element of [.0,1.] st [c,d] in dom f holds

( ( S

take f ; :: thesis: for a, b being Element of [.0,1.] holds

( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

A0: dom f = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;

let a, b be Element of [.0,1.]; :: thesis: ( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

cc: ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15;

AA: [a,b] in dom f by A0, ZFMISC_1:87;

( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )

proof

hence
( ( max (a,b) = 1 implies f . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies f . (a,b) = 0 ) )
; :: thesis: verum
thus
( max (a,b) = 1 implies f . (a,b) = min (a,b) )
:: thesis: ( max (a,b) <> 1 implies f . (a,b) = 0 )

( a <> 1 & b <> 1 )_{2}(a,b)
by A1, AA

.= 0 by XXREAL_1:1, SUBSET_1:def 8 ;

hence f . (a,b) = 0 ; :: thesis: verum

end;proof

assume B0:
max (a,b) <> 1
; :: thesis: f . (a,b) = 0
assume
max (a,b) = 1
; :: thesis: f . (a,b) = min (a,b)

then ( a = 1 or b = 1 ) by XXREAL_0:16;

then f . [a,b] = H_{1}(a,b)
by A1, AA

.= min (a,b) by SUBSET_1:def 8, cc ;

hence f . (a,b) = min (a,b) ; :: thesis: verum

end;then ( a = 1 or b = 1 ) by XXREAL_0:16;

then f . [a,b] = H

.= min (a,b) by SUBSET_1:def 8, cc ;

hence f . (a,b) = min (a,b) ; :: thesis: verum

( a <> 1 & b <> 1 )

proof

then f . [a,b] =
H
assume
( a = 1 or b = 1 )
; :: thesis: contradiction

end;.= 0 by XXREAL_1:1, SUBSET_1:def 8 ;

hence f . (a,b) = 0 ; :: thesis: verum