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 Def11
.= (len s) + (len <*f*>) by FINSEQ_1:35
.= (len s) + 1 by FINSEQ_1:56 ;
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
A5: k in NAT by ORDINAL1:def 13;

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

suppose A6: 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 Def11 ;
then k in dom (s @ x) by A3, A5, A6;
then A7: ((s @ x) ^ <*(f @ x)*>) . k = (s @ x) . k by FINSEQ_1:def 7
.= (s . k) @ x by A3, A6, Def11 ;
dom s = Seg (len s) by FINSEQ_1:def 3;
then A8: k in dom s by A3, A5, A6;
k <= len (s ^ <*f*>) by A4, Def11;
then ((s ^ <*f*>) @ x) . k = ((s ^ <*f*>) . k) @ x by A3, Def11;
hence ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A7, A8, FINSEQ_1:def 7; :: thesis: verum

end;

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

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

end;

end;

end;

len ((s @ x) ^ <*(f @ x)*>) = (len (s @ x)) + (len <*(f @ x)*>) by FINSEQ_1:35
.= (len s) + (len <*(f @ x)*>) by Def11
.= (len s) + 1 by FINSEQ_1:56 ;
hence (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*> by A1, A2, FINSEQ_1:18; :: thesis: verum