set C = [.0,1.];

defpred S_{1}[ Real, Real] means ( $1 = $2 & $2 = 0 );

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

deffunc H_{2}( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In (($2 to_power $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_{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 x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies f . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies f . (x,y) = y to_power x ) )

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

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

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

( ( a = b & b = 0 implies f . (a,b) = 1 ) & ( ( a > 0 or b > 0 ) implies f . (a,b) = b to_power a ) )

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 x, y being Element of [.0,1.] holds

( ( x = y & y = 0 implies f . (x,y) = 1 ) & ( ( x > 0 or y > 0 ) implies f . (x,y) = y to_power x ) )

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

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

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

( ( a = b & b = 0 implies f . (a,b) = 1 ) & ( ( a > 0 or b > 0 ) implies f . (a,b) = b to_power a ) )

proof

hence
( ( a = b & b = 0 implies f . (a,b) = 1 ) & ( ( a > 0 or b > 0 ) implies f . (a,b) = b to_power a ) )
; :: thesis: verum
thus
( a = b & b = 0 implies f . (a,b) = 1 )
:: thesis: ( ( a > 0 or b > 0 ) implies f . (a,b) = b to_power a )

then X1: b to_power a in [.0,1.] by PowerIn01;

not S_{1}[a,b]
by X0;

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

.= b to_power a by SUBSET_1:def 8, X1 ;

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

end;proof

assume X0:
( a > 0 or b > 0 )
; :: thesis: f . (a,b) = b to_power a
assume
( a = b & b = 0 )
; :: thesis: f . (a,b) = 1

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

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

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

end;then f . [a,b] = H

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

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

then X1: b to_power a in [.0,1.] by PowerIn01;

not S

then f . [a,b] = H

.= b to_power a by SUBSET_1:def 8, X1 ;

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