defpred S1[ object , object , object ] means ( ( $1 = $2 implies $3 = 1 ) & ( not $1 = $2 implies $3 = 0 ) );
A1: for x, y, z1, z2 being object st x in C1 & y in C2 & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2 ;
A2: for x, y, z being object st x in C1 & y in C2 & S1[x,y,z] holds
z in REAL by Lm6;
consider IT being PartFunc of [:C1,C2:],REAL such that
A3: ( ( for x, y being object holds
( [x,y] in dom IT iff ( x in C1 & y in C2 & ex z being object st S1[x,y,z] ) ) ) & ( for x, y being object st [x,y] in dom IT holds
S1[x,y,IT . (x,y)] ) ) from BINOP_1:sch 5(A2, A1);
 [:C1,C2:] c= dom IT
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in [:C1,C2:] or [x,y] in dom IT )
A4: ( not x = y implies ex z being set st
( ( x = y implies z = 1 ) & ( not x = y implies z = 0 ) ) ) ;
assume A5: [x,y] in [:C1,C2:] ; :: thesis: [x,y] in dom IT
then A6: y in C2 by ZFMISC_1:87;
x in C1 by A5, ZFMISC_1:87;
hence [x,y] in dom IT by A3, A6, A4; :: thesis: verum
end;
then A7: dom IT = [:C1,C2:] ;
rng IT c= [.0,1.]
proof
let c be object ; :: according to TARSKI:def 3 :: thesis: ( not c in rng IT or c in [.0,1.] )
assume c in rng IT ; :: thesis: c in [.0,1.]
then consider z being Element of [:C1,C2:] such that
A8: z in dom IT and
A9: c = IT . z by PARTFUN1:3;
consider x, y being object such that
x in C1 and
y in C2 and
A10: z = [x,y] by ZFMISC_1:def 2;
A11: ( 1 in [.0,1.] & 0 in [.0,1.] )
proof
reconsider A = [.0,jj.] as non empty closed_interval Subset of REAL by MEASURE5:14;
A12: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A13: 1 = upper_bound A by INTEGRA1:5;
0 = lower_bound A by A12, INTEGRA1:5;
hence ( 1 in [.0,1.] & 0 in [.0,1.] ) by A13, INTEGRA2:1; :: thesis: verum
end;
then A14: ( x <> y implies IT . (x,y) in [.0,1.] ) by A3, A8, A10;
( x = y implies IT . (x,y) in [.0,1.] ) by A3, A8, A10, A11;
hence c in [.0,1.] by A9, A10, A14; :: thesis: verum
end;
then IT is RMembership_Func of C1,C2 by A7, FUNCT_2:def 1, RELAT_1:def 19;
hence ex b1 being RMembership_Func of C1,C2 st
for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . (x,y) = 1 ) & ( x <> y implies b1 . (x,y) = 0 ) ) by A3, A7; :: thesis: verum