let G be RealNormSpace-Sequence; for h being FinSequence of (product G)
for y, x being Point of (product G)
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
let h be FinSequence of (product G); for y, x being Point of (product G)
for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
let y, x be Point of (product G); for y0, Z being Element of product (carr G)
for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
let y0, Z be Element of product (carr G); for j being Element of NAT st y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) holds
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
let j be Element of NAT ; ( y = y0 & Z = 0. (product G) & len h = (len G) + 1 & 1 <= j & j <= len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) implies x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) )
assume that
A1:
y = y0
and
A2:
Z = 0. (product G)
and
A3:
len h = (len G) + 1
and
A4:
( 1 <= j & j <= len G )
and
A5:
for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i)))
; x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
len G <= len h
by A3, NAT_1:11;
then
j <= len h
by A4, XXREAL_0:2;
then
j in Seg (len h)
by A4;
then
j in dom h
by FINSEQ_1:def 3;
then A6:
h /. j = Z +* (y0 | (Seg (((len G) + 1) -' j)))
by A5;
( 1 <= j + 1 & j + 1 <= len h )
by A3, A4, NAT_1:12, XREAL_1:6;
then
j + 1 in Seg (len h)
;
then
j + 1 in dom h
by FINSEQ_1:def 3;
then A7:
h /. (j + 1) = Z +* (y0 | (Seg (((len G) + 1) -' (j + 1))))
by A5;
j in Seg (len G)
by A4;
then
((len G) -' j) + 1 in Seg (len G)
by NAT_2:6;
then
((len G) + 1) -' j in Seg (len G)
by A4, NAT_D:38;
then
((len G) + 1) -' j in dom G
by FINSEQ_1:def 3;
then A8:
In ((((len G) + 1) -' j),(dom G)) = ((len G) + 1) -' j
by SUBSET_1:def 8;
set xh = x + (h /. (j + 1));
reconsider x1 = x, y1 = y as Element of product (carr G) by Th10;
reconsider xy = x + y as Element of product (carr G) by Th10;
x + (h /. (j + 1)) is Element of product (carr G)
by Th10;
then consider g being Function such that
A9:
( x + (h /. (j + 1)) = g & dom g = dom (carr G) & ( for y being object st y in dom (carr G) holds
g . y in (carr G) . y ) )
by CARD_3:def 5;
A10:
dom (x + (h /. (j + 1))) = dom G
by A9, Lm1;
(proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y) = xy . (((len G) + 1) -' j)
by A8, Def3;
then A11: (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) =
(x + (h /. (j + 1))) +* ((In ((((len G) + 1) -' j),(dom G))),(xy . (((len G) + 1) -' j)))
by Def4
.=
(x + (h /. (j + 1))) +* ((In ((((len G) + 1) -' j),(dom G))) .--> (xy . (((len G) + 1) -' j)))
by A10, FUNCT_7:def 3
.=
(x + (h /. (j + 1))) +* ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j)))
by A8, FUNCOP_1:def 9
;
reconsider F1 = x + (h /. j) as len G -element FinSequence ;
reconsider F2 = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) as len G -element FinSequence ;
reconsider h1 = h /. j as Element of product (carr G) by Th10;
reconsider xh1 = x + (h /. j) as Element of product (carr G) by Th10;
reconsider h2 = h /. (j + 1) as Element of product (carr G) by Th10;
A12:
( len F1 = len G & len F2 = len G )
by CARD_1:def 7;
for k being Nat st 1 <= k & k <= len F1 holds
F1 . k = F2 . k
proof
let k be
Nat;
( 1 <= k & k <= len F1 implies F1 . k = F2 . k )
assume A13:
( 1
<= k &
k <= len F1 )
;
F1 . k = F2 . k
then A14:
k in Seg (len F1)
;
then reconsider k1 =
k as
Element of
dom G by CARD_1:def 7, FINSEQ_1:def 3;
(proj k1) . xh1 = ((proj k1) . x) + ((proj k1) . (h /. j))
by Th35;
then A15:
F1 . k = ((proj k1) . x) + ((proj k1) . (h /. j))
by Def3;
y0 is
Element of the
carrier of
(product G)
by Th10;
then A16:
dom y0 = Seg (len G)
by FINSEQ_1:89;
A17:
(proj k1) . (h /. j) = h1 . k
by Def3;
A18:
dom (y0 | (Seg (((len G) + 1) -' j))) = (dom y0) /\ (Seg (((len G) + 1) -' j))
by RELAT_1:61;
A19:
the
carrier of
(product G) = product (carr G)
by Th10;
per cases
( not k in Seg (((len G) + 1) -' j) or k in Seg (((len G) + 1) -' j) )
;
suppose A20:
not
k in Seg (((len G) + 1) -' j)
;
F1 . k = F2 . kthen
not
k in dom (y0 | (Seg (((len G) + 1) -' j)))
by A18, XBOOLE_0:def 4;
then
(proj k1) . (h /. j) = Z . k
by A17, A6, FUNCT_4:11;
then A21:
(proj k1) . (h /. j) = (proj k1) . (0. (product G))
by A2, Def3;
( not 1
<= k or not
k <= ((len G) + 1) -' j )
by A20;
then
not
k in dom ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j)))
by A13, TARSKI:def 1;
then
((x + (h /. (j + 1))) +* ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j)))) . k1 = (x + (h /. (j + 1))) . k1
by FUNCT_4:11;
then A22:
F2 . k = (proj k1) . (x + (h /. (j + 1)))
by A19, A11, Def3;
A23:
(proj k1) . (h /. (j + 1)) = h2 . k
by Def3;
((len G) + 1) -' (j + 1) <= ((len G) + 1) -' j
by NAT_1:11, NAT_D:41;
then
Seg (((len G) + 1) -' (j + 1)) c= Seg (((len G) + 1) -' j)
by FINSEQ_1:5;
then
not
k in Seg (((len G) + 1) -' (j + 1))
by A20;
then
not
k in (dom y0) /\ (Seg (((len G) + 1) -' (j + 1)))
by XBOOLE_0:def 4;
then
not
k in dom (y0 | (Seg (((len G) + 1) -' (j + 1))))
by RELAT_1:61;
then
(Z +* (y0 | (Seg (((len G) + 1) -' (j + 1))))) . k = Z . k
by FUNCT_4:11;
then
(proj k1) . (h /. (j + 1)) = (proj k1) . (0. (product G))
by A2, A23, A7, Def3;
hence
F1 . k = F2 . k
by A21, A15, A22, Th35;
verum end; suppose A24:
k in Seg (((len G) + 1) -' j)
;
F1 . k = F2 . kthen A25:
k in dom (y0 | (Seg (((len G) + 1) -' j)))
by A18, A14, A16, A12, XBOOLE_0:def 4;
then
(proj k1) . (h /. j) = (y0 | (Seg (((len G) + 1) -' j))) . k
by A17, A6, FUNCT_4:13;
then
(proj k1) . (h /. j) = y0 . k
by A25, FUNCT_1:47;
then A26:
(proj k1) . (h /. j) = (proj k1) . y
by A1, Def3;
then A27:
F1 . k = (proj k1) . (x + y)
by A15, Th35;
per cases
( k = ((len G) + 1) -' j or k <> ((len G) + 1) -' j )
;
suppose A30:
k <> ((len G) + 1) -' j
;
F1 . k = F2 . kthen
not
k in dom ({(((len G) + 1) -' j)} --> (xy . (((len G) + 1) -' j)))
by TARSKI:def 1;
then
F2 . k = (x + (h /. (j + 1))) . k
by A11, FUNCT_4:11;
then A31:
F2 . k = (proj k1) . (x + (h /. (j + 1)))
by A19, Def3;
k <= ((len G) + 1) -' j
by A24, FINSEQ_1:1;
then
k < ((len G) + 1) -' j
by A30, XXREAL_0:1;
then
k <= (((len G) + 1) -' j) -' 1
by NAT_D:49;
then
k <= ((len G) + 1) -' (j + 1)
by NAT_2:30;
then
k in Seg (((len G) + 1) -' (j + 1))
by A13;
then A32:
k in dom (y0 | (Seg (((len G) + 1) -' (j + 1))))
by A14, A16, A12, RELAT_1:57;
(proj k1) . (h /. (j + 1)) = h2 . k
by Def3;
then
(proj k1) . (h /. (j + 1)) = (y0 | (Seg (((len G) + 1) -' (j + 1)))) . k1
by A7, A32, FUNCT_4:13;
then
(proj k1) . (h /. (j + 1)) = y0 . k
by A32, FUNCT_1:47;
then
(proj k1) . (h /. (j + 1)) = (proj k1) . y
by A1, Def3;
hence
F1 . k = F2 . k
by A26, A15, A31, Th35;
verum end; end;
end;
hence
x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y))
by A12; verum