let p be FuncSequence; :: thesis: for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence
let f be Function; :: thesis: ( rng f c= firstdom p implies <*f*> ^ p is FuncSequence )
assume A1: rng f c= firstdom p ; :: thesis: <*f*> ^ p is FuncSequence
consider q being FinSequence such that
A2: len q = (len p) + 1 and
A3: for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1))) by Def7;
set r = <*(dom f)*> ^ q;
A4: len <*(dom f)*> = 1 by FINSEQ_1:40;
A5: len <*f*> = 1 by FINSEQ_1:40;
then A6: len (<*f*> ^ p) = (len p) + 1 by FINSEQ_1:22;

A7: now :: thesis: ( p <> {} implies rng f c= q . 1 )

assume A8: p <> {} ; :: thesis: rng f c= q . 1
then len p >= 0 + 1 by NAT_1:13;
then 1 in dom p by FINSEQ_3:25;
then p . 1 in Funcs ((q . 1),(q . (1 + 1))) by A3;
then ex g being Function st
( p . 1 = g & dom g = q . 1 & rng g c= q . 2 ) by FUNCT_2:def 2;
hence rng f c= q . 1 by A1, A8, Def5; :: thesis: verum

end;

<*f*> ^ p is FuncSeq-like

proof

take <*(dom f)*> ^ q ; :: according to FUNCT_7:def 8 :: thesis: ( len (<*(dom f)*> ^ q) = (len (<*f*> ^ p)) + 1 & ( for i being Nat st i in dom (<*f*> ^ p) holds
(<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1))) ) )
1 <= len q by A2, NAT_1:11;
then A9: 1 in dom q by FINSEQ_3:25;
thus len (<*(dom f)*> ^ q) = (len (<*f*> ^ p)) + 1 by A2, A4, A6, FINSEQ_1:22; :: thesis: for i being Nat st i in dom (<*f*> ^ p) holds
(<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1)))
let i be Nat; :: thesis: ( i in dom (<*f*> ^ p) implies (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1))) )
assume A10: i in dom (<*f*> ^ p) ; :: thesis: (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1)))
then A11: i >= 1 by FINSEQ_3:25;
A12: rng f c= q . 1 by A1, A7, Th56;
A13: i <= (len p) + 1 by A6, A10, FINSEQ_3:25;

per cases ( i = 1 or i <> 1 ) ;

suppose A14: i = 1 ; :: thesis: (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1)))

then A15: ( (<*(dom f)*> ^ q) . i = dom f & (<*f*> ^ p) . i = f ) by FINSEQ_1:41;
(<*(dom f)*> ^ q) . (i + 1) = q . 1 by A4, A9, A14, FINSEQ_1:def 7;
hence (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1))) by A12, A15, FUNCT_2:def 2; :: thesis: verum

end;

suppose i <> 1 ; :: thesis: (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1)))

then i > 1 by A11, XXREAL_0:1;
then i >= 1 + 1 by NAT_1:13;
then consider j being Nat such that
A16: i = (1 + 1) + j by NAT_1:10;
A17: i = (j + 1) + 1 by A16;
then ( j + 1 >= 1 & j + 1 <= len p ) by A13, NAT_1:11, XREAL_1:6;
then A18: j + 1 in dom p by FINSEQ_3:25;
then A19: p . (j + 1) = (<*f*> ^ p) . i by A5, A17, FINSEQ_1:def 7;
A20: (j + 1) + 1 in dom q by A2, A18, Th22;
A21: p . (j + 1) in Funcs ((q . (j + 1)),(q . ((j + 1) + 1))) by A3, A18;
j + 1 in dom q by A2, A18, Th22;
then (<*(dom f)*> ^ q) . i = q . (j + 1) by A4, A16, A21, FINSEQ_1:def 7;
hence (<*f*> ^ p) . i in Funcs (((<*(dom f)*> ^ q) . i),((<*(dom f)*> ^ q) . (i + 1))) by A4, A16, A21, A20, A19, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence <*f*> ^ p is FuncSequence ; :: thesis: verum