let p be FinSequence; :: thesis: for x being set st x in rng p holds
p = ((p -| x) ^ <*x*>) ^ (p |-- x)
let x be set ; :: thesis: ( x in rng p implies p = ((p -| x) ^ <*x*>) ^ (p |-- x) )
assume A1: x in rng p ; :: thesis: p = ((p -| x) ^ <*x*>) ^ (p |-- x)
set q1 = p -| x;
set q2 = p |-- x;
set r = (p -| x) ^ <*x*>;
A2: len p = ((len p) - (x .. p)) + (x .. p)
.= (((x .. p) - 1) + 1) + (len (p |-- x)) by A1, Def7
.= ((len (p -| x)) + 1) + (len (p |-- x)) by A1, Th46
.= ((len (p -| x)) + (len <*x*>)) + (len (p |-- x)) by FINSEQ_1:57
.= (len ((p -| x) ^ <*x*>)) + (len (p |-- x)) by FINSEQ_1:35 ;

A3: now

let k be Element of 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

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:38;

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, Th48 ;
:: 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:4, 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 by FINSEQ_1:def 8
.= p . (((x .. p) - 1) + 1) by A1, Th29
.= p . k by A1, A7, A8, Th46 ;
:: thesis: verum

end;

end;

end;

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

end;

now

let k be Element of 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, Def7
.= p . (((len (p -| x)) + 1) + k) by A1, Th46
.= p . (((len (p -| x)) + (len <*x*>)) + k) by FINSEQ_1:57
.= p . ((len ((p -| x) ^ <*x*>)) + k) by FINSEQ_1:35 ;
hence p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k ; :: thesis: verum

end;

hence p = ((p -| x) ^ <*x*>) ^ (p |-- x) by A2, A3, FINSEQ_3:43; :: thesis: verum