defpred S₁[ 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) & S₁[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) & S₁[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) & S₁[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) & S₁[x,y] )

proof

take y ; :: thesis: ( y in bool (bool the carrier of FMT_R^1) & S₁[x,y] )
thus ( y in bool (bool the carrier of FMT_R^1) & S₁[x,y] ) ; :: thesis: verum

end;

hence ex y being object st
( y in bool (bool the carrier of FMT_R^1) & S₁[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
S₁[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
S₁[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 b₁ 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 & b₁ . r = Balls x ) ; :: thesis: verum