let X be RealNormSpace-Sequence; :: thesis: for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let x be Element of (product X); :: thesis: for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let Y be RealNormSpace; :: thesis: for z being Element of (product (X ^ <*Y*>))
for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let z be Element of (product (X ^ <*Y*>)); :: thesis: for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let j be Element of dom (X ^ <*Y*>); :: thesis: for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let y be Element of Y; :: thesis: for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>
let y0 be Point of Y; :: thesis: ( z = x ^ <*y0*> & j = (len x) + 1 implies (reproj (j,z)) . y = x ^ <*y*> )
assume A1: ( z = x ^ <*y0*> & j = (len x) + 1 ) ; :: thesis: (reproj (j,z)) . y = x ^ <*y*>
set CX = carr X;
A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
A3: ex x1 being Function st
( x = x1 & dom x1 = dom (carr X) & ( for i being object st i in dom (carr X) holds
x1 . i in (carr X) . i ) ) by A2, CARD_3:def 5;
dom x = Seg (len (carr X)) by A3, FINSEQ_1:def 3;
then A4: len x = len (carr X) by FINSEQ_1:def 3;
A5: len X = len (carr X) by PRVECT_1:def 11;
reconsider y1 = y as Element of ((X ^ <*Y*>) . j) by A1, A4, A5, FINSEQ_1:42;
A6: dom ((reproj (j,z)) . y1) = dom (z +* (j,y1)) by NDIFF_5:def 4
.= dom z by FUNCT_7:30 ;
then A7: dom ((reproj (j,z)) . y1) = Seg (len z) by FINSEQ_1:def 3;
A8: len z = (len x) + (len <*y0*>) by FINSEQ_1:22, A1
.= (len x) + 1 by FINSEQ_1:40 ;
then A9: len ((reproj (j,z)) . y1) = (len x) + 1 by A7, FINSEQ_1:def 3;
A10: len (x ^ <*y*>) = (len x) + (len <*y*>) by FINSEQ_1:22
.= (len x) + 1 by FINSEQ_1:40 ;
A11: dom ((reproj (j,z)) . y1) = dom (x ^ <*y*>) by A7, A8, A10, FINSEQ_1:def 3;
for k being object st k in dom ((reproj (j,z)) . y1) holds
((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k

proof

let k be object ; :: thesis: ( k in dom ((reproj (j,z)) . y1) implies ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k )
assume A12: k in dom ((reproj (j,z)) . y1) ; :: thesis: ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k
then A13: k in Seg (len ((reproj (j,z)) . y1)) by FINSEQ_1:def 3;
reconsider k1 = k as Nat by A12;
A14: ((reproj (j,z)) . y1) . k1 = (z +* (j,y1)) . k1 by NDIFF_5:def 4;
A15: ( 1 <= k1 & k1 <= len ((reproj (j,z)) . y1) ) by A13, FINSEQ_1:1;

per cases ( k1 <= len x or len x < k1 ) ;

suppose A16: k1 <= len x ; :: thesis: ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k

then k1 in Seg (len x) by A15;
then A17: k1 in dom x by FINSEQ_1:def 3;
A18: (len x) + 0 < (len x) + 1 by XREAL_1:8;
((reproj (j,z)) . y1) . k1 = z . k1 by A1, A14, A16, A18, FUNCT_7:32
.= x . k1 by A1, A17, FINSEQ_1:def 7 ;
hence ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k by A17, FINSEQ_1:def 7; :: thesis: verum

end;

suppose len x < k1 ; :: thesis: ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k

then (len x) + 1 <= k1 by NAT_1:13;
then A19: (len x) + 1 = k1 by A9, A15, XXREAL_0:1;
then (x ^ <*y*>) . k1 = y by FINSEQ_1:42;
hence ((reproj (j,z)) . y1) . k = (x ^ <*y*>) . k by A1, A6, A12, A14, A19, FUNCT_7:31; :: thesis: verum

end;

end;

end;

hence (reproj (j,z)) . y = x ^ <*y*> by FUNCT_1:2, A11; :: thesis: verum