let f1, f2 be Function of S,(TPlane (p,(0. (TOP-REAL n)))); :: thesis: ( ( for q being Point of (TOP-REAL n) st q in S holds
f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) & ( for q being Point of (TOP-REAL n) st q in S holds
f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ) implies f1 = f2 )
assume that
A8: for q being Point of (TOP-REAL n) st q in S holds
f1 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) and
A9: for q being Point of (TOP-REAL n) st q in S holds
f2 . q = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) ; :: thesis: f1 = f2
for x being object st x in [#] S holds
f1 . x = f2 . x

proof

let x be object ; :: thesis: ( x in [#] S implies f1 . x = f2 . x )
assume A10: x in [#] S ; :: thesis: f1 . x = f2 . x
[#] S c= [#] (TOP-REAL n) by PRE_TOPC:def 4;
then reconsider q = x as Point of (TOP-REAL n) by A10;
A11: q in S by A10;
thus f1 . x = (1 / (1 - |(q,p)|)) * (q - (|(q,p)| * p)) by A11, A8
.= f2 . x by A11, A9 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum