let D, D9, E be non empty set ; for d being Element of D
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let d be Element of D; for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let d9 be Element of D9; for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let F be Function of [:D,D9:],E; for p being FinSequence of D holds F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
let p be FinSequence of D; F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
set pd = p ^ <*d*>;
set q = F [:] (p,d9);
set r = F [:] ((p ^ <*d*>),d9);
set s = (F [:] (p,d9)) ^ <*(F . (d,d9))*>;
set i = len p;
A1:
len (F [:] (p,d9)) = len p
by FINSEQ_2:84;
len (p ^ <*d*>) = (len p) + 1
by FINSEQ_2:16;
then A2:
len (F [:] ((p ^ <*d*>),d9)) = (len p) + 1
by FINSEQ_2:84;
then A3:
dom (F [:] ((p ^ <*d*>),d9)) = Seg ((len p) + 1)
by FINSEQ_1:def 3;
A4:
now for j being Nat st j in dom (F [:] ((p ^ <*d*>),d9)) holds
(F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . jlet j be
Nat;
( j in dom (F [:] ((p ^ <*d*>),d9)) implies (F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j )assume A5:
j in dom (F [:] ((p ^ <*d*>),d9))
;
(F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . jnow F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . jper cases
( j in Seg (len p) or j = (len p) + 1 )
by A3, A5, FINSEQ_2:7;
suppose A6:
j in Seg (len p)
;
F . (((p ^ <*d*>) . j),d9) = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . jthen A7:
j in dom (F [:] (p,d9))
by A1, FINSEQ_1:def 3;
Seg (len p) = dom p
by FINSEQ_1:def 3;
hence F . (
((p ^ <*d*>) . j),
d9) =
F . (
(p . j),
d9)
by A6, FINSEQ_1:def 7
.=
(F [:] (p,d9)) . j
by A7, FUNCOP_1:27
.=
((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j
by A7, FINSEQ_1:def 7
;
verum end; end; end; hence
(F [:] ((p ^ <*d*>),d9)) . j = ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) . j
by A5, FUNCOP_1:27;
verum end;
len ((F [:] (p,d9)) ^ <*(F . (d,d9))*>) = (len (F [:] (p,d9))) + 1
by FINSEQ_2:16;
hence
F [:] ((p ^ <*d*>),d9) = (F [:] (p,d9)) ^ <*(F . (d,d9))*>
by A1, A2, A4, FINSEQ_2:9; verum