let p, q be Point of (TOP-REAL 2); ( p `1 <= q `1 implies proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).] )
assume A1:
p `1 <= q `1
; proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]
for y being object holds
( y in [.(p `1),(q `1).] iff ex x being object st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) )
proof
let y be
object ;
( y in [.(p `1),(q `1).] iff ex x being object st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) )
hereby ( ex x being object st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x ) implies y in [.(p `1),(q `1).] )
assume A2:
y in [.(p `1),(q `1).]
;
ex x being object st
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x )then reconsider r =
y as
Real ;
consider t being
Real such that A3:
0 <= t
and A4:
t <= 1
and A5:
r = (t * (p `1)) + ((1 - t) * (q `1))
by A1, A2, Th51;
set o =
(t * p) + ((1 - t) * q);
reconsider x =
(t * p) + ((1 - t) * q) as
object ;
take x =
x;
( x in dom proj1 & x in LSeg (p,q) & y = proj1 . x )
(t * p) + ((1 - t) * q) in the
carrier of
(TOP-REAL 2)
;
hence
x in dom proj1
by FUNCT_2:def 1;
( x in LSeg (p,q) & y = proj1 . x )
(t * p) + ((1 - t) * q) in LSeg (
q,
p)
by A3, A4;
hence
x in LSeg (
p,
q)
;
y = proj1 . xthus y =
((t * p) `1) + ((1 - t) * (q `1))
by A5, TOPREAL3:4
.=
((t * p) `1) + (((1 - t) * q) `1)
by TOPREAL3:4
.=
((t * p) + ((1 - t) * q)) `1
by TOPREAL3:2
.=
proj1 . x
by PSCOMP_1:def 5
;
verum
end;
given x being
object such that
x in dom proj1
and A6:
x in LSeg (
p,
q)
and A7:
y = proj1 . x
;
y in [.(p `1),(q `1).]
reconsider s =
x as
Point of
(TOP-REAL 2) by A6;
x in LSeg (
q,
p)
by A6;
then consider r being
Real such that A8:
s = ((1 - r) * q) + (r * p)
and A9:
0 <= r
and A10:
r <= 1
;
y =
s `1
by A7, PSCOMP_1:def 5
.=
(((1 - r) * q) `1) + ((r * p) `1)
by A8, TOPREAL3:2
.=
((1 - r) * (q `1)) + ((r * p) `1)
by TOPREAL3:4
.=
((1 - r) * (q `1)) + (r * (p `1))
by TOPREAL3:4
;
hence
y in [.(p `1),(q `1).]
by A1, A9, A10, Th51;
verum
end;
hence
proj1 .: (LSeg (p,q)) = [.(p `1),(q `1).]
by FUNCT_1:def 6; verum