let X be non empty set ; 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); 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); for x being Element of X holds (s ^ <*f*>) @ x = (s @ x) ^ <*(f @ x)*>
let x be Element of X; (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;
( 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)
;
((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 A8:
k = len ((s ^ <*f*>) @ x)
;
((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;
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; verum