let a be object ; :: thesis: for p being FinSequence st a in rng p holds
ex q, r being FinSequence st p = (q ^ <*a*>) ^ r
let p be FinSequence; :: thesis: ( a in rng p implies ex q, r being FinSequence st p = (q ^ <*a*>) ^ r )
assume a in rng p ; :: thesis: ex q, r being FinSequence st p = (q ^ <*a*>) ^ r
then consider i being object such that
A1: ( i in dom p & a = p . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A1;
A3: ( 1 <= i & i <= len p ) by A1, FINSEQ_3:25;
consider k being Nat such that
A2: i = 1 + k by NAT_1:10, A1, FINSEQ_3:25;
set q = (1,k) -cut p;
set r = ((i + 1),(len p)) -cut p;
take (1,k) -cut p ; :: thesis: ex r being FinSequence st p = (((1,k) -cut p) ^ <*a*>) ^ r
take ((i + 1),(len p)) -cut p ; :: thesis: p = (((1,k) -cut p) ^ <*a*>) ^ (((i + 1),(len p)) -cut p)
( k <= i & (i,i) -cut p = <*a*> ) by A1, A3, A2, NAT_1:11, FINSEQ_6:132;
hence p = (((1,k) -cut p) ^ <*a*>) ^ (((i + 1),(len p)) -cut p) by A3, A2, FINSEQ_6:136; :: thesis: verum