set C = [.0,1.];
defpred S1[ Real, Real] means \$1 + \$2 < 1;
deffunc H1( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In ((max (\$1,\$2)),[.0,1.]);
deffunc H2( 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
( ( S1[c,d] implies f . [c,d] = H1(c,d) ) & ( not S1[c,d] implies f . [c,d] = H2(c,d) ) ) from 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
( ( S1[c,d] implies f . [c,d] = H1(c,d) ) & ( not S1[c,d] implies f . [c,d] = H2(c,d) ) ) ;
take f ; :: thesis: for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies f . (a,b) = max (a,b) ) & ( a + b >= 1 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: ( ( a + b < 1 implies f . (a,b) = max (a,b) ) & ( a + b >= 1 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 ;
( ( a + b < 1 implies f . (a,b) = max (a,b) ) & ( a + b >= 1 implies f . (a,b) = 1 ) )
proof
thus ( a + b < 1 implies f . (a,b) = max (a,b) ) :: thesis: ( a + b >= 1 implies f . (a,b) = 1 )
proof
assume a + b < 1 ; :: thesis: f . (a,b) = max (a,b)
then f . [a,b] = H1(a,b) by A1, AA
.= max (a,b) by ;
hence f . (a,b) = max (a,b) ; :: thesis: verum
end;
assume a + b >= 1 ; :: thesis: f . (a,b) = 1
then f . [a,b] = H2(a,b) by A1, AA
.= 1 by ;
hence f . (a,b) = 1 ; :: thesis: verum
end;
hence ( ( a + b < 1 implies f . (a,b) = max (a,b) ) & ( a + b >= 1 implies f . (a,b) = 1 ) ) ; :: thesis: verum