let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st not f is empty holds

L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

let p be Point of (TOP-REAL 2); :: thesis: ( not f is empty implies L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) )

set q = f /. 1;

A1: len <*p*> = 1 by FINSEQ_1:39;

then A2: len (<*p*> ^ f) = 1 + (len f) by FINSEQ_1:22;

assume A3: not f is empty ; :: thesis: L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

assume A15: x in (LSeg (p,(f /. 1))) \/ (L~ f) ; :: thesis: x in L~ (<*p*> ^ f)

then reconsider r = x as Point of (TOP-REAL 2) ;

L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

let p be Point of (TOP-REAL 2); :: thesis: ( not f is empty implies L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) )

set q = f /. 1;

A1: len <*p*> = 1 by FINSEQ_1:39;

then A2: len (<*p*> ^ f) = 1 + (len f) by FINSEQ_1:22;

assume A3: not f is empty ; :: thesis: L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (LSeg (p,(f /. 1))) \/ (L~ f) c= L~ (<*p*> ^ f)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg (p,(f /. 1))) \/ (L~ f) or x in L~ (<*p*> ^ f) )let x be object ; :: thesis: ( x in L~ (<*p*> ^ f) implies x in (LSeg (p,(f /. 1))) \/ (L~ f) )

assume A4: x in L~ (<*p*> ^ f) ; :: thesis: x in (LSeg (p,(f /. 1))) \/ (L~ f)

then reconsider r = x as Point of (TOP-REAL 2) ;

consider i being Nat such that

A5: 1 <= i and

A6: i + 1 <= len (<*p*> ^ f) and

A7: r in LSeg (((<*p*> ^ f) /. i),((<*p*> ^ f) /. (i + 1))) by A4, Th14;

end;assume A4: x in L~ (<*p*> ^ f) ; :: thesis: x in (LSeg (p,(f /. 1))) \/ (L~ f)

then reconsider r = x as Point of (TOP-REAL 2) ;

consider i being Nat such that

A5: 1 <= i and

A6: i + 1 <= len (<*p*> ^ f) and

A7: r in LSeg (((<*p*> ^ f) /. i),((<*p*> ^ f) /. (i + 1))) by A4, Th14;

now :: thesis: ( ( i = 1 & r in LSeg (p,(f /. 1)) ) or ( i > 1 & r in L~ f ) )end;

hence
x in (LSeg (p,(f /. 1))) \/ (L~ f)
by XBOOLE_0:def 3; :: thesis: verumper cases
( i = 1 or i > 1 )
by A5, XXREAL_0:1;

end;

case A8:
i = 1
; :: thesis: r in LSeg (p,(f /. 1))

then A9:
p = (<*p*> ^ f) /. i
by FINSEQ_5:15;

i in dom f by A3, A8, FINSEQ_5:6;

hence r in LSeg (p,(f /. 1)) by A1, A7, A8, A9, FINSEQ_4:69; :: thesis: verum

end;i in dom f by A3, A8, FINSEQ_5:6;

hence r in LSeg (p,(f /. 1)) by A1, A7, A8, A9, FINSEQ_4:69; :: thesis: verum

case A10:
i > 1
; :: thesis: r in L~ f

then consider j being Nat such that

A11: i = j + 1 by NAT_1:6;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A12: 1 <= j by A10, A11, NAT_1:13;

A13: j + 1 <= len f by A2, A6, A11, XREAL_1:6;

then j + 1 in dom f by A12, SEQ_4:134;

then A14: (<*p*> ^ f) /. (i + 1) = f /. (j + 1) by A1, A11, FINSEQ_4:69;

j in dom f by A12, A13, SEQ_4:134;

then (<*p*> ^ f) /. i = f /. j by A1, A11, FINSEQ_4:69;

hence r in L~ f by A7, A12, A13, A14, Th15; :: thesis: verum

end;A11: i = j + 1 by NAT_1:6;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A12: 1 <= j by A10, A11, NAT_1:13;

A13: j + 1 <= len f by A2, A6, A11, XREAL_1:6;

then j + 1 in dom f by A12, SEQ_4:134;

then A14: (<*p*> ^ f) /. (i + 1) = f /. (j + 1) by A1, A11, FINSEQ_4:69;

j in dom f by A12, A13, SEQ_4:134;

then (<*p*> ^ f) /. i = f /. j by A1, A11, FINSEQ_4:69;

hence r in L~ f by A7, A12, A13, A14, Th15; :: thesis: verum

assume A15: x in (LSeg (p,(f /. 1))) \/ (L~ f) ; :: thesis: x in L~ (<*p*> ^ f)

then reconsider r = x as Point of (TOP-REAL 2) ;

per cases
( r in LSeg (p,(f /. 1)) or r in L~ f )
by A15, XBOOLE_0:def 3;

end;

suppose A16:
r in LSeg (p,(f /. 1))
; :: thesis: x in L~ (<*p*> ^ f)

set i = 1;

1 <= len f by A3, NAT_1:14;

then A17: 1 + 1 <= len (<*p*> ^ f) by A2, XREAL_1:6;

1 in dom f by A3, FINSEQ_5:6;

then A18: f /. 1 = (<*p*> ^ f) /. (1 + 1) by A1, FINSEQ_4:69;

p = (<*p*> ^ f) /. 1 by FINSEQ_5:15;

hence x in L~ (<*p*> ^ f) by A16, A17, A18, Th15; :: thesis: verum

end;1 <= len f by A3, NAT_1:14;

then A17: 1 + 1 <= len (<*p*> ^ f) by A2, XREAL_1:6;

1 in dom f by A3, FINSEQ_5:6;

then A18: f /. 1 = (<*p*> ^ f) /. (1 + 1) by A1, FINSEQ_4:69;

p = (<*p*> ^ f) /. 1 by FINSEQ_5:15;

hence x in L~ (<*p*> ^ f) by A16, A17, A18, Th15; :: thesis: verum

suppose
r in L~ f
; :: thesis: x in L~ (<*p*> ^ f)

then consider j being Nat such that

A19: 1 <= j and

A20: j + 1 <= len f and

A21: r in LSeg ((f /. j),(f /. (j + 1))) by Th14;

set i = j + 1;

j in dom f by A19, A20, SEQ_4:134;

then A22: (<*p*> ^ f) /. (j + 1) = f /. j by A1, FINSEQ_4:69;

j + 1 in dom f by A19, A20, SEQ_4:134;

then A23: (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by A1, FINSEQ_4:69;

(j + 1) + 1 <= len (<*p*> ^ f) by A2, A20, XREAL_1:6;

hence x in L~ (<*p*> ^ f) by A21, A22, A23, Th15, NAT_1:12; :: thesis: verum

end;A19: 1 <= j and

A20: j + 1 <= len f and

A21: r in LSeg ((f /. j),(f /. (j + 1))) by Th14;

set i = j + 1;

j in dom f by A19, A20, SEQ_4:134;

then A22: (<*p*> ^ f) /. (j + 1) = f /. j by A1, FINSEQ_4:69;

j + 1 in dom f by A19, A20, SEQ_4:134;

then A23: (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by A1, FINSEQ_4:69;

(j + 1) + 1 <= len (<*p*> ^ f) by A2, A20, XREAL_1:6;

hence x in L~ (<*p*> ^ f) by A21, A22, A23, Th15, NAT_1:12; :: thesis: verum