set C = [.0,1.];
deffunc H1( Element of [.0,1.], Element of [.0,1.]) -> Element of [.0,1.] = In (((($1 + $2) - ((2 * $1) * $2)) / (1 - ($1 * $2))),[.0,1.]);
defpred S1[ set , set ] means ( $1 = 1 & $2 = 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] = H2(c,d) ) & ( not S1[c,d] implies f . [c,d] = H1(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
( ( S1[c,d] implies f . [c,d] = H2(c,d) ) & ( not S1[c,d] implies f . [c,d] = H1(c,d) ) )
;
take
f
; for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies f . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )
A0:
dom f = [:[.0,1.],[.0,1.]:]
by FUNCT_2:def 1;
let a, b be Element of [.0,1.]; ( ( a = b & b = 1 implies f . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )
AA:
[a,b] in dom f
by A0, ZFMISC_1:87;
( ( a = b & b = 1 implies f . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )
proof
thus
(
a = b &
b = 1 implies
f . (
a,
b)
= 1 )
( ( a <> 1 or b <> 1 ) implies f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) )
assume
(
a <> 1 or
b <> 1 )
;
f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b))
then f . [a,b] =
H1(
a,
b)
by A1, AA
.=
((a + b) - ((2 * a) * b)) / (1 - (a * b))
by SUBSET_1:def 8, HamCoIn01
;
hence
f . (
a,
b)
= ((a + b) - ((2 * a) * b)) / (1 - (a * b))
;
verum
end;
hence
( ( a = b & b = 1 implies f . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies f . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )
; verum