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)
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 (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 ) )
per cases ( i = 1 or i > 1 ) by A5, XXREAL_0:1;
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;
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;
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 (TOP-REAL 2) ;
per cases ( r in LSeg (p,(f /. 1)) or r in L~ f ) by A15, XBOOLE_0:def 3;
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;
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;
end;