let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( not f1 is empty & not f2 is empty implies L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) )
set p = f1 /. (len f1);
set q = f2 /. 1;
defpred S₁[ FinSequence of (TOP-REAL 2)] means L~ ((f1 ^ <*(f2 /. 1)*>) ^ $1) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ $1));
assume A1: not f1 is empty ; :: thesis: ( f2 is empty or L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) )
A2: for f being FinSequence of (TOP-REAL 2)
for o being Point of (TOP-REAL 2) st S₁[f] holds
S₁[f ^ <*o*>]

proof

let f be FinSequence of (TOP-REAL 2); :: thesis: for o being Point of (TOP-REAL 2) st S₁[f] holds
S₁[f ^ <*o*>]
let o be Point of (TOP-REAL 2); :: thesis: ( S₁[f] implies S₁[f ^ <*o*>] )
assume A3: S₁[f] ; :: thesis: S₁[f ^ <*o*>]

per cases ( f is empty or not f is empty ) ;

suppose f is empty ; :: thesis: S₁[f ^ <*o*>]

then A4: f ^ <*o*> = <*o*> by FINSEQ_1:34;
len (f1 ^ <*(f2 /. 1)*>) = (len f1) + 1 by FINSEQ_2:16;
then (f1 ^ <*(f2 /. 1)*>) /. (len (f1 ^ <*(f2 /. 1)*>)) = f2 /. 1 by FINSEQ_4:67;
hence L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = (L~ (f1 ^ <*(f2 /. 1)*>)) \/ (LSeg ((f2 /. 1),o)) by A4, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (LSeg ((f2 /. 1),o)) by A1, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1),o*>) by Th21
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A4, FINSEQ_1:def 9 ;
:: thesis: verum

end;

suppose A5: not f is empty ; :: thesis: S₁[f ^ <*o*>]

set g = (f1 ^ <*(f2 /. 1)*>) ^ f;
set h = <*(f2 /. 1)*> ^ f;
len f <> 0 by A5;
then consider f9 being FinSequence of (TOP-REAL 2), d being Point of (TOP-REAL 2) such that
A6: f = f9 ^ <*d*> by FINSEQ_2:19;
A7: <*(f2 /. 1)*> ^ f = (<*(f2 /. 1)*> ^ f9) ^ <*d*> by A6, FINSEQ_1:32;
then len (<*(f2 /. 1)*> ^ f) = (len (<*(f2 /. 1)*> ^ f9)) + 1 by FINSEQ_2:16;
then A8: (<*(f2 /. 1)*> ^ f) /. (len (<*(f2 /. 1)*> ^ f)) = d by A7, FINSEQ_4:67;
A9: (f1 ^ <*(f2 /. 1)*>) ^ f = ((f1 ^ <*(f2 /. 1)*>) ^ f9) ^ <*d*> by A6, FINSEQ_1:32;
then len ((f1 ^ <*(f2 /. 1)*>) ^ f) = (len ((f1 ^ <*(f2 /. 1)*>) ^ f9)) + 1 by FINSEQ_2:16;
then ((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f)) = d by A9, FINSEQ_4:67;
then A10: (L~ (<*(f2 /. 1)*> ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) = L~ ((<*(f2 /. 1)*> ^ f) ^ <*o*>) by A8, Th19
.= L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>)) by FINSEQ_1:32 ;
thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = L~ (((f1 ^ <*(f2 /. 1)*>) ^ f) ^ <*o*>) by FINSEQ_1:32
.= (L~ ((f1 ^ <*(f2 /. 1)*>) ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) by Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A3, A10, XBOOLE_1:4 ; :: thesis: verum

end;

end;

end;

assume not f2 is empty ; :: thesis: L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)
then A11: f2 = <*(f2 /. 1)*> ^ (f2 /^ 1) by FINSEQ_5:29;
A12: S₁[ <*> the carrier of (TOP-REAL 2)]

proof

set O = <*> the carrier of (TOP-REAL 2);
thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (<*> the carrier of (TOP-REAL 2))) = L~ (f1 ^ <*(f2 /. 1)*>) by FINSEQ_1:34
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ {} by A1, Th19
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1)*>) by Th12
.= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (<*> the carrier of (TOP-REAL 2)))) by FINSEQ_1:34 ; :: thesis: verum

end;

for f being FinSequence of (TOP-REAL 2) holds S₁[f] from FINSEQ_2:sch 2(A12, A2);
then L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f2 /^ 1)) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f2 /^ 1))) ;
hence L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) by A11, FINSEQ_1:32; :: thesis: verum