set C = [.0,1.];
defpred S₁[ set , set ] means ( $1 = 0 or $2 = 0 );
deffunc H₁( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((max ($1,$2)),[.0,1.]);
deffunc H₂( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In (1,[.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₁[c,d] implies f . [c,d] = H₁(c,d) ) & ( not S₁[c,d] implies f . [c,d] = H₂(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₁[c,d] implies f . [c,d] = H₁(c,d) ) & ( not S₁[c,d] implies f . [c,d] = H₂(c,d) ) ) ;
take f ; :: thesis: for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies f . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies f . (a,b) = 1 ) )
A0: dom f = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1;
let a, b be Element of [.0,1.]; :: thesis: ( ( min (a,b) = 0 implies f . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies f . (a,b) = 1 ) )
cc: ( max (a,b) = a or max (a,b) = b ) by XXREAL_0:16;
AA: [a,b] in dom f by A0, ZFMISC_1:87;
( ( min (a,b) = 0 implies f . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies f . (a,b) = 1 ) )

proof

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

proof

assume min (a,b) = 0 ; :: thesis: f . (a,b) = max (a,b)
then ( a = 0 or b = 0 ) by XXREAL_0:15;
then f . [a,b] = H₁(a,b) by A1, AA
.= max (a,b) by SUBSET_1:def 8, cc ;
hence f . (a,b) = max (a,b) ; :: thesis: verum

end;

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

proof

assume ( a = 0 or b = 0 ) ; :: thesis: contradiction

per cases then ( a = 0 or b = 0 ) ;

suppose Z1: a = 0 ; :: thesis: contradiction

then b >= a by XXREAL_1:1;
hence contradiction by B0, XXREAL_0:def 9, Z1; :: thesis: verum

end;

suppose Z1: b = 0 ; :: thesis: contradiction

then a >= b by XXREAL_1:1;
hence contradiction by B0, XXREAL_0:def 9, Z1; :: thesis: verum

end;

end;

end;

then f . [a,b] = H₂(a,b) by A1, AA
.= 1 by XXREAL_1:1, SUBSET_1:def 8 ;
hence f . (a,b) = 1 ; :: thesis: verum

end;

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