let X be non empty set ; :: thesis: for s being FinSequence of (bspace X)
for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let s be FinSequence of (bspace X); :: thesis: for f being Element of (bspace X)
for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let f be Element of (bspace X); :: thesis: for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let x be Element of X; :: thesis: (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
set L = (s ^ <*f*>) @ x;
set R = (s @ x) ^ <*(f @ x)*>;
A1: len ((s ^ <*f*>) @ x) = len (s ^ <*f*>) by Def9
.= (len s) + (len <*f*>) by FINSEQ_1:22
.= (len s) + 1 by FINSEQ_1:39 ;
A2: for k being Nat st 1 <= k & k <= len ((s ^ <*f*>) @ x) holds
((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((s ^ <*f*>) @ x) implies ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k )
assume that
A3: 1 <= k and
A4: k <= len ((s ^ <*f*>) @ x) ; :: thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k

per cases ( k <= len s or k = len ((s ^ <*f*>) @ x) ) by A1, A4, NAT_1:8;

suppose A5: k <= len s ; :: thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k

dom (s @ x) = Seg (len (s @ x)) by FINSEQ_1:def 3
.= Seg (len s) by Def9 ;
then k in dom (s @ x) by A3, A5;
then A6: ((s @ x) ^ <*(f @ x)*>) . k = (s @ x) . k by FINSEQ_1:def 7
.= (s . k) @ x by A3, A5, Def9 ;
dom s = Seg (len s) by FINSEQ_1:def 3;
then A7: k in dom s by A3, A5;
k <= len (s ^ <*f*>) by A4, Def9;
then ((s ^ <*f*>) @ x) . k = ((s ^ <*f*>) . k) @ x by A3, Def9;
hence ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A6, A7, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A8: k = len ((s ^ <*f*>) @ x) ; :: thesis: ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k

dom <*(f @ x)*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A9: 1 in dom <*(f @ x)*> by TARSKI:def 1;
len (s @ x) = len s by Def9;
then A10: ((s @ x) ^ <*(f @ x)*>) . k = <*(f @ x)*> . 1 by A1, A8, A9, FINSEQ_1:def 7
.= f @ x ;
dom <*f*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*f*> by TARSKI:def 1;
then A11: (s ^ <*f*>) . k = <*f*> . 1 by A1, A8, FINSEQ_1:def 7
.= f ;
k <= len (s ^ <*f*>) by A4, Def9;
hence ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A3, A10, A11, Def9; :: thesis: verum

end;

end;

end;

len ((s @ x) ^ <*(f @ x)*>) = (len (s @ x)) + (len <*(f @ x)*>) by FINSEQ_1:22
.= (len s) + (len <*(f @ x)*>) by Def9
.= (len s) + 1 by FINSEQ_1:39 ;
hence (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*> by A1, A2; :: thesis: verum