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 i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let x be Element of (product X); :: thesis: for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let Y be RealNormSpace; :: thesis: for z being Element of (product (X ^ <*Y*>))
for i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let z be Element of (product (X ^ <*Y*>)); :: thesis: for i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let i be Element of dom X; :: thesis: for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let j be Element of dom (X ^ <*Y*>); :: thesis: for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let xi be Element of (X . i); :: thesis: for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>
let y be Point of Y; :: thesis: ( i = j & z = x ^ <*y*> implies (reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*> )
assume A1: ( i = j & z = x ^ <*y*> ) ; :: thesis: (reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*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
( x1 = x & 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;
i in dom X ;
then i in Seg (len X) by FINSEQ_1:def 3;
then A6: ( 1 <= i & i <= len X ) by FINSEQ_1:1;
reconsider xj = xi as Element of ((X ^ <*Y*>) . j) by A1, FINSEQ_1:def 7;
A7: dom ((reproj (j,z)) . xj) = dom (z +* (j,xj)) by NDIFF_5:def 4
.= dom z by FUNCT_7:30 ;
then dom ((reproj (j,z)) . xj) = Seg (len z) by FINSEQ_1:def 3;
then A8: len ((reproj (j,z)) . xj) = len z by FINSEQ_1:def 3;
A9: dom ((reproj (i,x)) . xi) = dom (x +* (i,xi)) by NDIFF_5:def 4
.= dom x by FUNCT_7:30 ;
then A10: dom ((reproj (i,x)) . xi) = Seg (len x) by FINSEQ_1:def 3;
then A11: len ((reproj (i,x)) . xi) = len x by FINSEQ_1:def 3;
A12: len z = (len x) + (len <*y*>) by FINSEQ_1:22, A1
.= (len x) + 1 by FINSEQ_1:40 ;
A13: len (((reproj (i,x)) . xi) ^ <*y*>) = (len ((reproj (i,x)) . xi)) + (len <*y*>) by FINSEQ_1:22
.= (len ((reproj (i,x)) . xi)) + 1 by FINSEQ_1:40 ;
A14: dom (((reproj (i,x)) . xi) ^ <*y*>) = Seg (len (((reproj (i,x)) . xi) ^ <*y*>)) by FINSEQ_1:def 3
.= Seg (len ((reproj (j,z)) . xj)) by A8, A10, A12, A13, FINSEQ_1:def 3
.= dom ((reproj (j,z)) . xj) by FINSEQ_1:def 3 ;
for k being object st k in dom (((reproj (i,x)) . xi) ^ <*y*>) holds
(((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k

proof

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

per cases ( k1 <= len ((reproj (i,x)) . xi) or len ((reproj (i,x)) . xi) < k1 ) ;

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

then A19: k1 in Seg (len ((reproj (i,x)) . xi)) by A18;
then k1 in dom ((reproj (i,x)) . xi) by FINSEQ_1:def 3;
then A20: (((reproj (i,x)) . xi) ^ <*y*>) . k1 = ((reproj (i,x)) . xi) . k1 by FINSEQ_1:def 7
.= (x +* (i,xi)) . k1 by NDIFF_5:def 4 ;
A21: k1 in dom x by A9, A19, FINSEQ_1:def 3;

per cases ( k1 = i or k1 <> i ) ;

suppose A22: k1 = i ; :: thesis: (((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k

then (((reproj (i,x)) . xi) ^ <*y*>) . k1 = xi by A20, A21, FUNCT_7:31;
hence (((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k by A1, A7, A14, A15, A17, A22, FUNCT_7:31; :: thesis: verum

end;

suppose A24: k1 <> i ; :: thesis: (((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k

((reproj (j,z)) . xj) . k1 = z . k1 by A1, A17, A24, FUNCT_7:32
.= x . k1 by A1, A21, FINSEQ_1:def 7 ;
hence (((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k by A20, A24, FUNCT_7:32; :: thesis: verum

end;

end;

end;

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

then A26: (len ((reproj (i,x)) . xi)) + 1 <= k1 by NAT_1:13;
then A27: (len ((reproj (i,x)) . xi)) + 1 = k1 by A18, XXREAL_0:1;
A28: j <> k1 by A1, A4, A5, A6, A10, A25, FINSEQ_1:def 3;
A29: (len x) + 1 = k1 by A11, A18, A26, XXREAL_0:1;
((reproj (j,z)) . xj) . k1 = z . k1 by A17, A28, FUNCT_7:32
.= y by A1, A29, FINSEQ_1:42 ;
hence (((reproj (i,x)) . xi) ^ <*y*>) . k = ((reproj (j,z)) . xj) . k by A27, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

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