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

.= (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

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

len ((s @ x) ^ <*(f @ x)*>) =
(len (s @ x)) + (len <*(f @ x)*>)
by FINSEQ_1:22
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

end;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;

end;

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;.= 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

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 by FINSEQ_1:def 8 ;

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 by FINSEQ_1:def 8 ;

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;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 by FINSEQ_1:def 8 ;

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 by FINSEQ_1:def 8 ;

k <= len (s ^ <*f*>) by A4, Def9;

hence ((s ^ <*f*>) @ x) . k = ((s @ x) ^ <*(f @ x)*>) . k by A3, A10, A11, Def9; :: thesis: verum

.= (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