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

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

hence
f1 = f2
by FUNCT_2:12; :: thesis: verum
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;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