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) )
assume A1: not f is empty ; :: thesis: L~ (<*p*> ^ f) = (LSeg p,(f /. 1)) \/ (L~ f)
set q = f /. 1;
A2: len f <> 0 by A1;
A3: len <*p*> = 1 by FINSEQ_1:56;
then A4: len (<*p*> ^ f) = 1 + (len f) by FINSEQ_1:35;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (LSeg p,(f /. 1)) \/ (L~ f) c= L~ (<*p*> ^ f)
let x be set ; :: thesis: ( x in L~ (<*p*> ^ f) implies x in (LSeg p,(f /. 1)) \/ (L~ f) )
assume A5: 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 Element of NAT such that
A6: 1 <= i and
A7: i + 1 <= len (<*p*> ^ f) and
A8: r in LSeg ((<*p*> ^ f) /. i),((<*p*> ^ f) /. (i + 1)) by A5, Th14;
now
per cases ( i = 1 or i > 1 ) by A6, XXREAL_0:1;
case A11: i > 1 ; :: thesis: r in L~ f
then consider j being Nat such that
A12: i = j + 1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A13: 1 <= j by A11, A12, NAT_1:13;
A14: j + 1 <= len f by A4, A7, A12, XREAL_1:8;
then j in dom f by A13, GOBOARD2:3;
then A15: (<*p*> ^ f) /. i = f /. j by A3, A12, FINSEQ_4:84;
j + 1 in dom f by A13, A14, GOBOARD2:3;
then (<*p*> ^ f) /. (i + 1) = f /. (j + 1) by A3, A12, FINSEQ_4:84;
hence r in L~ f by A8, A13, A14, A15, 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LSeg p,(f /. 1)) \/ (L~ f) or x in L~ (<*p*> ^ f) )
assume A16: 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 A16, XBOOLE_0:def 3;
suppose A17: r in LSeg p,(f /. 1) ; :: thesis: x in L~ (<*p*> ^ f)
set i = 1;
1 <= len f by A2, NAT_1:14;
then A18: 1 + 1 <= len (<*p*> ^ f) by A4, XREAL_1:8;
A19: p = (<*p*> ^ f) /. 1 by FINSEQ_5:16;
1 in dom f by A1, FINSEQ_5:6;
then f /. 1 = (<*p*> ^ f) /. (1 + 1) by A3, FINSEQ_4:84;
hence x in L~ (<*p*> ^ f) by A17, A18, A19, Th15; :: thesis: verum
end;
suppose r in L~ f ; :: thesis: x in L~ (<*p*> ^ f)
then consider j being Element of NAT such that
A20: 1 <= j and
A21: j + 1 <= len f and
A22: r in LSeg (f /. j),(f /. (j + 1)) by Th14;
set i = j + 1;
A23: (j + 1) + 1 <= len (<*p*> ^ f) by A4, A21, XREAL_1:8;
j in dom f by A20, A21, GOBOARD2:3;
then A24: (<*p*> ^ f) /. (j + 1) = f /. j by A3, FINSEQ_4:84;
j + 1 in dom f by A20, A21, GOBOARD2:3;
then (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by A3, FINSEQ_4:84;
hence x in L~ (<*p*> ^ f) by A22, A23, A24, Th15, NAT_1:12; :: thesis: verum
end;
end;