let p be FinSequence; :: thesis: for x being object st x in rng p holds
p = ((p -| x) ^ <*x*>) ^ (p |-- x)
let x be object ; :: thesis: ( x in rng p implies p = ((p -| x) ^ <*x*>) ^ (p |-- x) )
set q1 = p -| x;
set q2 = p |-- x;
set r = (p -| x) ^ <*x*>;
assume A1: x in rng p ; :: thesis: p = ((p -| x) ^ <*x*>) ^ (p |-- x)

A2: now :: thesis: for k being Nat st k in dom (p |-- x) holds
p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k

let k be Nat; :: thesis: ( k in dom (p |-- x) implies p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k )
assume k in dom (p |-- x) ; :: thesis: p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k
then (p |-- x) . k = p . ((((x .. p) - 1) + 1) + k) by A1, Def6
.= p . (((len (p -| x)) + 1) + k) by A1, Th34
.= p . (((len (p -| x)) + (len <*x*>)) + k) by FINSEQ_1:40
.= p . ((len ((p -| x) ^ <*x*>)) + k) by FINSEQ_1:22 ;
hence p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k ; :: thesis: verum

end;

A3: now :: thesis: for k being Nat st k in dom ((p -| x) ^ <*x*>) holds
p . k = ((p -| x) ^ <*x*>) . k

let k be Nat; :: thesis: ( k in dom ((p -| x) ^ <*x*>) implies p . k = ((p -| x) ^ <*x*>) . k )
assume A4: k in dom ((p -| x) ^ <*x*>) ; :: thesis: p . k = ((p -| x) ^ <*x*>) . k

now :: thesis: ((p -| x) ^ <*x*>) . k = p . k

per cases ( k in dom (p -| x) or ex n being Nat st
( n in dom <*x*> & k = (len (p -| x)) + n ) ) by A4, FINSEQ_1:25;

suppose A5: k in dom (p -| x) ; :: thesis: ((p -| x) ^ <*x*>) . k = p . k

hence ((p -| x) ^ <*x*>) . k = (p -| x) . k by FINSEQ_1:def 7
.= p . k by A1, A5, Th36 ;
:: thesis: verum

end;

suppose ex n being Nat st
( n in dom <*x*> & k = (len (p -| x)) + n ) ; :: thesis: ((p -| x) ^ <*x*>) . k = p . k

then consider n being Nat such that
A6: n in dom <*x*> and
A7: k = (len (p -| x)) + n ;
n in {1} by A6, FINSEQ_1:2, FINSEQ_1:def 8;
then A8: n = 1 by TARSKI:def 1;
hence ((p -| x) ^ <*x*>) . k = <*x*> . 1 by A6, A7, FINSEQ_1:def 7
.= x
.= p . (((x .. p) - 1) + 1) by A1, Th19
.= p . k by A1, A7, A8, Th34 ;
:: thesis: verum

end;

end;

end;

hence p . k = ((p -| x) ^ <*x*>) . k ; :: thesis: verum

end;

len p = ((len p) - (x .. p)) + (x .. p)
.= (((x .. p) - 1) + 1) + (len (p |-- x)) by A1, Def6
.= ((len (p -| x)) + 1) + (len (p |-- x)) by A1, Th34
.= ((len (p -| x)) + (len <*x*>)) + (len (p |-- x)) by FINSEQ_1:40
.= (len ((p -| x) ^ <*x*>)) + (len (p |-- x)) by FINSEQ_1:22 ;
hence p = ((p -| x) ^ <*x*>) ^ (p |-- x) by A3, A2, FINSEQ_3:38; :: thesis: verum