defpred S1[ object , object ] means ex x being Point of (TopSpaceMetr RealSpace) st
( x = $1 & $2 = Balls x );
A1: for x being object st x in the carrier of FMT_R^1 holds
ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of FMT_R^1 implies ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S1[x,y] ) )
assume A2: x in the carrier of FMT_R^1 ; :: thesis: ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S1[x,y] )
reconsider z = x as Element of (TopSpaceMetr RealSpace) by A2, FINTOPO7:def 15, TOPMETR:def 6;
reconsider BZ = Balls z as Subset-Family of (TopSpaceMetr RealSpace) ;
reconsider y = Balls z as Element of bool (bool the carrier of FMT_R^1) by FINTOPO7:def 15, TOPMETR:def 6;
ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S1[x,y] )
proof
take y ; :: thesis: ( y in bool (bool the carrier of FMT_R^1) & S1[x,y] )
thus ( y in bool (bool the carrier of FMT_R^1) & S1[x,y] ) ; :: thesis: verum
end;
hence ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S1[x,y] ) ; :: thesis: verum
end;
ex f being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st
for x being object st x in the carrier of FMT_R^1 holds
S1[x,f . x] from FUNCT_2:sch 1(A1);
 then consider f being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) such that
A3: for x being object st x in the carrier of FMT_R^1 holds
S1[x,f . x] ;
for r being Real ex y being Point of (TopSpaceMetr RealSpace) st
( r = y & f . r = Balls y ) by A3, Th52, XREAL_0:def 1;
hence ex b1 being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st
for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & b1 . r = Balls x ) ; :: thesis: verum