let m be non zero Nat; :: thesis:
let h be FinSequence of REAL m; :: thesis:
let y, x be Element of REAL m; :: thesis:
let j be Nat; :: thesis:
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)) ) ) ; :: thesis:
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 :: thesis:

let n be Nat; :: thesis:
assume A15: ( 1 <= n & n <= len rep ) ; :: thesis:
then 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 by XXREAL_0:1;

suppose A20: n < (m + 1) -' j ; :: thesis:

then 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; :: thesis:

end;

suppose A26: n = (m + 1) -' j ; :: thesis:

then 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 ; :: thesis:

end;

suppose A30: n > (m + 1) -' j ; :: thesis:

then 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; :: thesis:

end;

hence x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y)) by A14; :: thesis: