let x be REAL -valued FinSequence; for i being Nat
for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>
let i be Nat; for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>
let I0 be set ; ( I0 c= Seg i & Seg (i + 1) c= dom x implies Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*> )
assume A1:
( I0 c= Seg i & Seg (i + 1) c= dom x )
; Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>
A4:
Seg i c= Seg (i + 1)
by NAT_1:11, FINSEQ_1:5;
then A17:
I0 c= dom x
by A1;
A6:
dom (x | (i + 1)) = Seg (i + 1)
by A1, RELAT_1:62;
then A7:
{(i + 1)} c= dom (x | (i + 1))
by FINSEQ_1:4, ZFMISC_1:31;
A8:
I0 c= Seg (i + 1)
by A4, A1;
then A9:
I0 \/ {(i + 1)} c= Seg (i + 1)
by A7, A6, XBOOLE_1:8;
A10: Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) =
Seq (x | (I0 \/ {(i + 1)}))
by A8, A7, A6, XBOOLE_1:8, RELAT_1:74
.=
(x | (I0 \/ {(i + 1)})) * (Sgm (dom (x | (I0 \/ {(i + 1)}))))
;
A11:
I0 \/ {(i + 1)} c= dom x
by A1, A9;
then A12:
dom (x | (I0 \/ {(i + 1)})) = I0 \/ {(i + 1)}
by RELAT_1:62;
( i < i + 1 & i + 1 in Seg (i + 1) )
by FINSEQ_1:4, NAT_1:16;
then A13:
Sgm (I0 \/ {(i + 1)}) = (Sgm I0) ^ <*(i + 1)*>
by A1, LM040;
A14:
dom (x | (I0 \/ {(i + 1)})) = I0 \/ {(i + 1)}
by RELAT_1:62, A11;
rng (x | (I0 \/ {(i + 1)})) c= REAL
;
then reconsider f = x | (I0 \/ {(i + 1)}) as Function of (I0 \/ {(i + 1)}),REAL by A14, FUNCT_2:2;
I0 is included_in_Seg
by A1, FINSEQ_1:def 13;
then A19:
rng (Sgm I0) = I0
by FINSEQ_1:def 14;
then reconsider p = Sgm I0 as FinSequence of I0 \/ {(i + 1)} by FINSEQ_1:def 4, XBOOLE_1:10;
i + 1 in {(i + 1)}
by TARSKI:def 1;
then reconsider d = i + 1 as Element of I0 \/ {(i + 1)} by XBOOLE_0:def 3;
A15:
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (f * p) ^ <*(f . d)*>
by FINSEQOP:8, A13, A10, A12;
f * p =
(x | I0) * (Sgm I0)
by LM050, A19
.=
Seq ((x | I0) | I0)
by A17, RELAT_1:62
.=
Seq ((x | i),I0)
by A1, RELAT_1:74
;
hence
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>
by A15, FUNCT_1:49; verum