let m be non zero Nat; for h being FinSequence of REAL m
for y, x being Element of REAL m
for j being Nat st len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) holds
x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
let h be FinSequence of REAL m; for y, x being Element of REAL m
for j being Nat st len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) holds
x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
let y, x be Element of REAL m; for j being Nat st len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) holds
x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
let j be Nat; ( len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) implies x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y)) )
assume A1:
( len h = m + 1 & 1 <= j & j <= m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) )
; x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
reconsider mj = m - j as Nat by A1, NAT_1:21;
reconsider xxx = (x /. ((m + 1) -' j)) + (y /. ((m + 1) -' j)) as Element of REAL ;
m <= m + 1
by NAT_1:11;
then A2:
Seg m c= Seg (m + 1)
by FINSEQ_1:5;
A3:
j in Seg m
by A1;
then
j in Seg (m + 1)
by A2;
then
j in dom h
by A1, FINSEQ_1:def 3;
then A4:
h /. j = (y | ((m + 1) -' j)) ^ (0* (j -' 1))
by A1;
j + 1 in Seg (m + 1)
by A3, FINSEQ_1:60;
then
j + 1 in dom h
by A1, FINSEQ_1:def 3;
then A5:
h /. (j + 1) = (y | ((m + 1) -' (j + 1))) ^ (0* ((j + 1) -' 1))
by A1;
(m + 1) -' j = (m -' j) + 1
by A1, NAT_D:38;
then A6:
1 <= (m + 1) -' j
by NAT_1:11;
A7:
1 - j <= 0
by A1, XREAL_1:47;
(m + 1) -' j =
(m + 1) - j
by A1, NAT_D:37
.=
m + (1 - j)
;
then A8:
(m + 1) -' j <= m
by A7, XREAL_1:32;
then
(m + 1) -' j in Seg m
by A6;
then A9:
( (m + 1) -' j in dom (x + y) & (m + 1) -' j in dom y & (m + 1) -' j in dom x )
by FINSEQ_1:89;
(m + 1) -' j <= len y
by A8, CARD_1:def 7;
then A10:
len (y | ((m + 1) -' j)) = (m + 1) -' j
by FINSEQ_1:59;
j + 1 <= m + 1
by A1, XREAL_1:6;
then A11:
(m + 1) -' (j + 1) = (m + 1) - (j + 1)
by XREAL_1:233;
then
( (m + 1) -' (j + 1) = m - j & j >= 0 )
;
then
(m + 1) -' (j + 1) <= m
by XREAL_1:43;
then
(m + 1) -' (j + 1) <= len y
by CARD_1:def 7;
then A12:
len (y | ((m + 1) -' (j + 1))) = (m + 1) -' (j + 1)
by FINSEQ_1:59;
(proj (((m + 1) -' j),m)) . (x + y) =
(x + y) . ((m + 1) -' j)
by PDIFF_1:def 1
.=
(x . ((m + 1) -' j)) + (y . ((m + 1) -' j))
by A9, VALUED_1:def 1
.=
(x . ((m + 1) -' j)) + (y /. ((m + 1) -' j))
by A9, PARTFUN1:def 6
.=
(x /. ((m + 1) -' j)) + (y /. ((m + 1) -' j))
by A9, PARTFUN1:def 6
;
then A13:
(reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y)) = Replace ((x + (h /. (j + 1))),((m + 1) -' j),xxx)
by PDIFF_1:def 5;
(reproj (((m + 1) -' j),(x + (h /. (j + 1))))) /. ((proj (((m + 1) -' j),m)) . (x + y)) is Element of REAL m
;
then reconsider rep = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) /. ((proj (((m + 1) -' j),m)) . (x + y)) as FinSequence of REAL ;
reconsider hj = h /. j as Element of REAL m ;
reconsider hj1 = h /. (j + 1) as Element of REAL m ;
A14: len (x + hj) =
m
by CARD_1:def 7
.=
len rep
by CARD_1:def 7
;
now for n being Nat st 1 <= n & n <= len rep holds
(x + (h /. j)) . n = rep . nlet n be
Nat;
( 1 <= n & n <= len rep implies (x + (h /. j)) . b1 = rep . b1 )assume A15:
( 1
<= n &
n <= len rep )
;
(x + (h /. j)) . b1 = rep . b1then A16:
( 1
<= n &
n <= m )
by CARD_1:def 7;
then
n in Seg m
;
then A17:
(
n in Seg (len (x + (h /. j))) &
n in Seg (len (x + (h /. (j + 1)))) &
n in Seg (len x) &
n in Seg (len y) )
by CARD_1:def 7;
then A18:
(
n in dom (x + (h /. j)) &
n in dom (x + (h /. (j + 1))) &
n in dom rep &
n in dom x &
n in dom y )
by A14, FINSEQ_1:def 3;
then A19:
(
(x + (h /. j)) . n = (x . n) + (hj . n) &
(x + (h /. (j + 1))) . n = (x . n) + (hj1 . n) )
by VALUED_1:def 1;
per cases
( n < (m + 1) -' j or n = (m + 1) -' j or n > (m + 1) -' j )
by XXREAL_0:1;
suppose A20:
n < (m + 1) -' j
;
(x + (h /. j)) . b1 = rep . b1then A21:
n in Seg ((m + 1) -' j)
by A15;
A22:
hj . n =
(y | (Seg ((m + 1) -' j))) . n
by A4, A10, A15, A20, FINSEQ_1:64
.=
y . n
by A21, FUNCT_1:49
;
m <= m + 1
by NAT_1:11;
then
n < (m + 1) - j
by A1, A20, XREAL_1:233, XXREAL_0:2;
then
n < mj + 1
;
then A23:
n <= mj
by NAT_1:13;
then A24:
n in Seg mj
by A15;
A25:
hj1 . n =
(y | (Seg mj)) . n
by A11, A23, A12, A5, A15, FINSEQ_1:64
.=
y . n
by A24, FUNCT_1:49
;
(
n <> (m + 1) -' j &
n <= len (x + (h /. (j + 1))) )
by A20, A17, FINSEQ_1:1;
then
rep /. n = (x + (h /. (j + 1))) /. n
by A13, A15, FINSEQ_7:10;
then rep . n =
(x + (h /. (j + 1))) /. n
by A18, PARTFUN1:def 6
.=
(x + (h /. (j + 1))) . n
by A18, PARTFUN1:def 6
;
hence
(x + (h /. j)) . n = rep . n
by A19, A25, A22;
verum end; suppose A26:
n = (m + 1) -' j
;
(x + (h /. j)) . b1 = rep . b1then A27:
n in Seg ((m + 1) -' j)
by A15;
A28:
hj . n =
(y | (Seg ((m + 1) -' j))) . n
by A4, A10, A15, A26, FINSEQ_1:64
.=
y . n
by A27, FUNCT_1:49
;
n <= len (x + (h /. (j + 1)))
by A17, FINSEQ_1:1;
then
rep /. n = (x /. n) + (y /. n)
by A26, A13, A15, FINSEQ_7:8;
then A29:
rep . n = (x /. n) + (y /. n)
by A18, PARTFUN1:def 6;
thus (x + (h /. j)) . n =
(x /. n) + (y . n)
by A18, A19, A28, PARTFUN1:def 6
.=
rep . n
by A29, A18, PARTFUN1:def 6
;
verum end; suppose A30:
n > (m + 1) -' j
;
(x + (h /. j)) . b1 = rep . b1then reconsider nm =
n - ((m + 1) -' j) as
Nat by NAT_1:21;
A31:
m <= m + 1
by NAT_1:11;
n <= len hj
by A16, CARD_1:def 7;
then A32:
hj . n =
(0* (j -' 1)) . nm
by A4, A10, A30, FINSEQ_1:24
.=
0
;
A33:
len y = m
by CARD_1:def 7;
j + 1
<= m + 1
by A1, XREAL_1:6;
then (m + 1) -' (j + 1) =
(m + 1) - (j + 1)
by XREAL_1:233
.=
m - j
.=
m -' j
by A1, XREAL_1:233
;
then A34:
len (y | ((m + 1) -' (j + 1))) = m -' j
by A33, FINSEQ_1:59, NAT_D:35;
n > (m + 1) - j
by A30, A31, A1, XREAL_1:233, XXREAL_0:2;
then
(
n > (m - j) + 1 &
(m - j) + 1
> (m - j) + 0 )
by XREAL_1:8;
then
n > m - j
by XXREAL_0:2;
then A35:
n > m -' j
by A1, XREAL_1:233;
then reconsider nmj =
n - (m -' j) as
Nat by NAT_1:21;
n <= len hj1
by A16, CARD_1:def 7;
then A36:
hj1 . n =
(0* ((j + 1) -' 1)) . (n - (m -' j))
by A5, A34, A35, FINSEQ_1:24
.=
0
;
(
n <> (m + 1) -' j &
n <= len (x + (h /. (j + 1))) )
by A30, A17, FINSEQ_1:1;
then
rep /. n = (x + (h /. (j + 1))) /. n
by A13, A15, FINSEQ_7:10;
then rep . n =
(x + (h /. (j + 1))) /. n
by A18, PARTFUN1:def 6
.=
(x + (h /. (j + 1))) . n
by A18, PARTFUN1:def 6
;
hence
(x + (h /. j)) . n = rep . n
by A19, A36, A32;
verum end; end;
hence
x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y))
by A14; verum