let f be FinSequence of (); :: thesis: for p being Point of () st not f is empty holds
L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

let p be Point of (); :: 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 ; :: 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 () ;
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 ;
now :: thesis: ( ( i = 1 & r in LSeg (p,(f /. 1)) ) or ( i > 1 & r in L~ f ) )
per cases ( i = 1 or i > 1 ) by ;
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 ;
hence r in LSeg (p,(f /. 1)) by ; :: thesis: verum
end;
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 ;
A13: j + 1 <= len f by ;
then j + 1 in dom f by ;
then A14: (<*p*> ^ f) /. (i + 1) = f /. (j + 1) by ;
j in dom f by ;
then (<*p*> ^ f) /. i = f /. j by ;
hence r in L~ f by A7, A12, A13, A14, Th15; :: thesis: verum
end;
end;
end;
hence x in (LSeg (p,(f /. 1))) \/ (L~ f) by XBOOLE_0:def 3; :: thesis: verum
end;
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) )
assume A15: x in (LSeg (p,(f /. 1))) \/ (L~ f) ; :: thesis: x in L~ (<*p*> ^ f)
then reconsider r = x as Point of () ;
per cases ( r in LSeg (p,(f /. 1)) or r in L~ f ) by ;
suppose A16: r in LSeg (p,(f /. 1)) ; :: thesis: x in L~ (<*p*> ^ f)
set i = 1;
1 <= len f by ;
then A17: 1 + 1 <= len (<*p*> ^ f) by ;
1 in dom f by ;
then A18: f /. 1 = (<*p*> ^ f) /. (1 + 1) by ;
p = (<*p*> ^ f) /. 1 by FINSEQ_5:15;
hence x in L~ (<*p*> ^ f) by ; :: thesis: verum
end;
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 ;
then A22: (<*p*> ^ f) /. (j + 1) = f /. j by ;
j + 1 in dom f by ;
then A23: (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by ;
(j + 1) + 1 <= len (<*p*> ^ f) by ;
hence x in L~ (<*p*> ^ f) by ; :: thesis: verum
end;
end;