let f1, f2 be Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)); :: thesis: ( ( for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & f1 . r = Balls x ) ) & ( for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & f2 . r = Balls x ) ) implies f1 = f2 )
assume that
A4: for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & f1 . r = Balls x ) and
A5: for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & f2 . r = Balls x ) ; :: thesis: f1 = f2
now :: thesis: ( dom f1 = dom f2 & ( for x being object st x in dom f1 holds
f1 . x = f2 . x ) )
dom f1 = the carrier of FMT_R^1 by FUNCT_2:def 1;
hence dom f1 = dom f2 by FUNCT_2:def 1; :: thesis: for x being object st x in dom f1 holds
f1 . x = f2 . x
hereby :: thesis: verum
let x be object ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; :: thesis: f1 . x = f2 . x
then reconsider r = x as Real ;
consider x1 being Point of (TopSpaceMetr RealSpace) such that
A6: r = x1 and
A7: f1 . r = Balls x1 by A4;
consider x2 being Point of (TopSpaceMetr RealSpace) such that
A8: r = x2 and
A9: f2 . r = Balls x2 by A5;
thus f1 . x = f2 . x by A6, A7, A8, A9; :: thesis: verum
end;
end;
hence f1 = f2 by FUNCT_1:2; :: thesis: verum