let p be FuncSequence; for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence
let f be Function; ( rng f c= firstdom p implies <*f*> ^ p is FuncSequence )
assume A1:
rng f c= firstdom p
; <*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;
<*f*> ^ p is FuncSeq-like
proof
take
<*(dom f)*> ^ q
;
FUNCT_7:def 8 ( 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;
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;
( 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)
;
(<*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
i <> 1
;
(<*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;
verum end; end;
end;
hence
<*f*> ^ p is FuncSequence
; verum